Theorem nanbi12i

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

	Ref	Expression
Hypotheses	nanbii.1	|- ( ph <-> ps )
	nanbi12i.2	|- ( ch <-> th )
Assertion	nanbi12i	|- ( ( ph -/\ ch ) <-> ( ps -/\ th ) )

Proof

Step	Hyp	Ref	Expression
1		nanbii.1	|- ( ph <-> ps )
2		nanbi12i.2	|- ( ch <-> th )
3		nanbi12	|- ( ( ( ph <-> ps ) /\ ( ch <-> th ) ) -> ( ( ph -/\ ch ) <-> ( ps -/\ th ) ) )
4	1 2 3	mp2an	|- ( ( ph -/\ ch ) <-> ( ps -/\ th ) )