Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for BJ
Propositional calculus
Logical equivalence
bj-dfbi5
Next ⟩
bj-dfbi6
Metamath Proof Explorer
Ascii
Unicode
Theorem
bj-dfbi5
Description:
Alternate definition of the biconditional.
(Contributed by
BJ
, 4-Oct-2019)
Ref
Expression
Assertion
bj-dfbi5
⊢
φ
↔
ψ
↔
φ
∨
ψ
→
φ
∧
ψ
Proof
Step
Hyp
Ref
Expression
1
orcom
⊢
φ
∧
ψ
∨
¬
φ
∨
ψ
↔
¬
φ
∨
ψ
∨
φ
∧
ψ
2
bj-dfbi4
⊢
φ
↔
ψ
↔
φ
∧
ψ
∨
¬
φ
∨
ψ
3
imor
⊢
φ
∨
ψ
→
φ
∧
ψ
↔
¬
φ
∨
ψ
∨
φ
∧
ψ
4
1
2
3
3bitr4i
⊢
φ
↔
ψ
↔
φ
∨
ψ
→
φ
∧
ψ