The Logic Resource Center

The Logic Resource Center

Public Alpha

The Logic Resource Center

Public Alpha

© 2025 The Logic Resource Center, LLC

Biconditional Elimination

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

Start a Problem →

Biconditional Elimination

i.

ϕ↔ψ

ii.

ψ

⋮

iii.

ϕ

↔E: i, ii

i.

ϕ↔ψ

ii.

ϕ

⋮

iii.

ψ

↔E: i, ii

Forward

Select a biconditional
Select an available instance of the formula on one of its sides
Click "Apply"

Forward, Adding Antecedent as Goal

Select a biconditional
Specify the side you want to make into a goal
Click "Apply"

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