Theorem 3anbi123d

Description: Deduction joining 3 equivalences to form equivalence of conjunctions. (Contributed by NM, 22-Apr-1994)

	Ref	Expression
Hypotheses	bi3d.1	|- ( ph -> ( ps <-> ch ) )
	bi3d.2	|- ( ph -> ( th <-> ta ) )
	bi3d.3	|- ( ph -> ( et <-> ze ) )
Assertion	3anbi123d	|- ( ph -> ( ( ps /\ th /\ et ) <-> ( ch /\ ta /\ ze ) ) )

Proof

Step	Hyp	Ref	Expression
1		bi3d.1	|- ( ph -> ( ps <-> ch ) )
2		bi3d.2	|- ( ph -> ( th <-> ta ) )
3		bi3d.3	|- ( ph -> ( et <-> ze ) )
4	1 2	anbi12d	|- ( ph -> ( ( ps /\ th ) <-> ( ch /\ ta ) ) )
5	4 3	anbi12d	|- ( ph -> ( ( ( ps /\ th ) /\ et ) <-> ( ( ch /\ ta ) /\ ze ) ) )
6		df-3an	|- ( ( ps /\ th /\ et ) <-> ( ( ps /\ th ) /\ et ) )
7		df-3an	|- ( ( ch /\ ta /\ ze ) <-> ( ( ch /\ ta ) /\ ze ) )
8	5 6 7	3bitr4g	|- ( ph -> ( ( ps /\ th /\ et ) <-> ( ch /\ ta /\ ze ) ) )