Metamath Proof Explorer

Theorem biimpor

Description: A rewriting rule for biconditional. (Contributed by Giovanni Mascellani, 15-Sep-2017)

Ref Expression
Assertion biimpor ⊢ φ ↔ ψ → χ ↔ ¬ φ ↔ ψ ∨ χ

Proof

Step Hyp Ref Expression
1 imor ⊢ φ ↔ ψ → χ ↔ ¬ φ ↔ ψ ∨ χ
2 notbinot2 ⊢ ¬ φ ↔ ψ ↔ ¬ φ ↔ ψ
3 2 orbi1i ⊢ ¬ φ ↔ ψ ∨ χ ↔ ¬ φ ↔ ψ ∨ χ
4 1 3 bitri ⊢ φ ↔ ψ → χ ↔ ¬ φ ↔ ψ ∨ χ