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 φ ψ θ χ τ