Theorem nanbi12i

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

	Ref	Expression
Hypotheses	nanbii.1	⊢ ( 𝜑 ↔ 𝜓 )
	nanbi12i.2	⊢ ( 𝜒 ↔ 𝜃 )
Assertion	nanbi12i	⊢ ( ( 𝜑 ⊼ 𝜒 ) ↔ ( 𝜓 ⊼ 𝜃 ) )

Proof

Step	Hyp	Ref	Expression
1		nanbii.1	⊢ ( 𝜑 ↔ 𝜓 )
2		nanbi12i.2	⊢ ( 𝜒 ↔ 𝜃 )
3		nanbi12	⊢ ( ( ( 𝜑 ↔ 𝜓 ) ∧ ( 𝜒 ↔ 𝜃 ) ) → ( ( 𝜑 ⊼ 𝜒 ) ↔ ( 𝜓 ⊼ 𝜃 ) ) )
4	1 2 3	mp2an	⊢ ( ( 𝜑 ⊼ 𝜒 ) ↔ ( 𝜓 ⊼ 𝜃 ) )