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