Theorem nanbi12

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

	Ref	Expression
Assertion	nanbi12	⊢ ( ( ( 𝜑 ↔ 𝜓 ) ∧ ( 𝜒 ↔ 𝜃 ) ) → ( ( 𝜑 ⊼ 𝜒 ) ↔ ( 𝜓 ⊼ 𝜃 ) ) )

Proof

Step	Hyp	Ref	Expression
1		nanbi1	⊢ ( ( 𝜑 ↔ 𝜓 ) → ( ( 𝜑 ⊼ 𝜒 ) ↔ ( 𝜓 ⊼ 𝜒 ) ) )
2		nanbi2	⊢ ( ( 𝜒 ↔ 𝜃 ) → ( ( 𝜓 ⊼ 𝜒 ) ↔ ( 𝜓 ⊼ 𝜃 ) ) )
3	1 2	sylan9bb	⊢ ( ( ( 𝜑 ↔ 𝜓 ) ∧ ( 𝜒 ↔ 𝜃 ) ) → ( ( 𝜑 ⊼ 𝜒 ) ↔ ( 𝜓 ⊼ 𝜃 ) ) )