This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nanbi12d

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

Ref Expression
Hypotheses nanbid.1 ⊢ φ → ψ ↔ χ
nanbi12d.2 ⊢ φ → θ ↔ τ
Assertion nanbi12d ⊢ φ → ψ ⊼ θ ↔ χ ⊼ τ

Proof

Step Hyp Ref Expression
1 nanbid.1 ⊢ φ → ψ ↔ χ
2 nanbi12d.2 ⊢ φ → θ ↔ τ
3 nanbi12 ⊢ ψ ↔ χ ∧ θ ↔ τ → ψ ⊼ θ ↔ χ ⊼ τ
4 1 2 3 syl2anc ⊢ φ → ψ ⊼ θ ↔ χ ⊼ τ