The Logic Resource Center
Public Alpha
Systems
Open options
Systems
The Logic Resource Center
Public Alpha
Systems
Open options
Systems
Biconditional Elimination
Constants
↔
Systems
LRC_F
The Logic Book
LRC
LRC_P
LRC_O
Start a Problem
→
Biconditional Elimination
i
i.
↔
ϕ
ψ
ii
ii.
ψ
⋮
i, ii
iii.
ϕ
↔E: i, ii
i
i.
↔
ϕ
ψ
ii
ii.
ϕ
⋮
i, ii
iii.
ψ
↔E: i, ii
Forward
Enter the formula you wish to add
Cite a biconditional and a formula that appars on one of its sides
Hit Return
Preview shown for the
Typed Forward Strict
derivation type in the
LRC_P
system
