Theorem 3anbi123d 1243

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

Hypotheses

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

Assertion

Ref	Expression
3anbi123d	|- ( ph -> ( ( ps /\ th /\ et ) <-> ( ch /\ ta /\ ze ) ) )

Proof of Theorem 3anbi123d

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

Syntax hints:   -> wi 4   /\ wa 102   <-> wb 103   /\ w3a 919

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115  df-3an 921

This theorem is referenced by:  3anbi12d  1244  3anbi13d  1245  3anbi23d  1246  limeq  4132  smoeq  5928  tfrlemi1  5969  ereq1  6136  elinp  6664  iccshftr  9016  iccshftl  9018  iccdil  9020  icccntr  9022  fzaddel  9077  elfzomelpfzo  9240  divalglemnn  10318  divalglemeunn  10321  divalglemeuneg  10323  dfgcd2  10403