Metamath Proof Explorer

Theorem nanbi12

Description: Join two logical equivalences with anti-conjunction. (Contributed by SF, 2-Jan-2018)

Ref Expression
Assertion nanbi12 ⊢ φ ↔ ψ ∧ χ ↔ θ → φ ⊼ χ ↔ ψ ⊼ θ

Proof

Step Hyp Ref Expression
1 nanbi1 ⊢ φ ↔ ψ → φ ⊼ χ ↔ ψ ⊼ χ
2 nanbi2 ⊢ χ ↔ θ → ψ ⊼ χ ↔ ψ ⊼ θ
3 1 2 sylan9bb ⊢ φ ↔ ψ ∧ χ ↔ θ → φ ⊼ χ ↔ ψ ⊼ θ