The Logic Resource Center

The Logic Resource Center

Public Alpha

The Logic Resource Center

Public Alpha

© 2025 The Logic Resource Center, LLC

Biconditional Introduction

Constants: ↔
Systems: LRC_F OLI The Logic Book LRC LRC_P LRC_O

Start a Problem →

Biconditional Introduction

i.

ϕ→ψ

ii.

ψ→ϕ

⋮

iii.

ϕ↔ψ

↔I: i, ii

i.

ϕ

A

⋮

ii.

ψ

Goal

iii.

ψ

A

⋮

iv.

ϕ

Goal

⋮

v.

ϕ↔ψ

↔I: i, ii, iii, iv

Forward, from Conditionals

Select an available conditional
Select another that has the sides reversed
Click "Apply"

Backward, to Sub-Proofs

Select a goal biconditional
Click "Apply"

Preview shown for the Point And Click derivation type in the LRC_F system