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 ( 𝜑 → ( ( 𝜓𝜃 ) ↔ ( 𝜒𝜏 ) ) )