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