Theorem nanbi12d

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

	Ref	Expression
Hypotheses	nanbid.1	|- ( ph -> ( ps <-> ch ) )
	nanbi12d.2	|- ( ph -> ( th <-> ta ) )
Assertion	nanbi12d	|- ( ph -> ( ( ps -/\ th ) <-> ( ch -/\ ta ) ) )

Proof

Step	Hyp	Ref	Expression
1		nanbid.1	|- ( ph -> ( ps <-> ch ) )
2		nanbi12d.2	|- ( ph -> ( th <-> ta ) )
3		nanbi12	|- ( ( ( ps <-> ch ) /\ ( th <-> ta ) ) -> ( ( ps -/\ th ) <-> ( ch -/\ ta ) ) )
4	1 2 3	syl2anc	|- ( ph -> ( ( ps -/\ th ) <-> ( ch -/\ ta ) ) )