Theorem 3anbi123d 1302

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 465	. . 3 |- ( ph -> ( ( ps /\ th ) <-> ( ch /\ ta ) ) )
4		bi3d.3	. . 3 |- ( ph -> ( et <-> ze ) )
5	3, 4	anbi12d 465	. 2 |- ( ph -> ( ( ( ps /\ th ) /\ et ) <-> ( ( ch /\ ta ) /\ ze ) ) )
6		df-3an 970	. 2 |- ( ( ps /\ th /\ et ) <-> ( ( ps /\ th ) /\ et ) )
7		df-3an 970	. 2 |- ( ( ch /\ ta /\ ze ) <-> ( ( ch /\ ta ) /\ ze ) )
8	5, 6, 7	3bitr4g 222	1 |- ( ph -> ( ( ps /\ th /\ et ) <-> ( ch /\ ta /\ ze ) ) )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104   /\ w3a 968

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

This theorem depends on definitions:  df-bi 116  df-3an 970

This theorem is referenced by:  3anbi12d  1303  3anbi13d  1304  3anbi23d  1305  limeq  4354  smoeq  6254  tfrlemi1  6296  tfr1onlemaccex  6312  tfrcllemaccex  6325  ereq1  6504  updjud  7043  ctssdclemr  7073  elinp  7411  sup3exmid  8848  iccshftr  9926  iccshftl  9928  iccdil  9930  icccntr  9932  fzaddel  9990  elfzomelpfzo  10162  seq3f1olemstep  10432  seq3f1olemp  10433  sumeq1  11292  summodclem2  11319  summodc  11320  zsumdc  11321  prodmodclem2  11514  prodmodc  11515  divalglemnn  11851  divalglemeunn  11854  divalglemeuneg  11856  dfgcd2  11943  pythagtriplem18  12209  pythagtriplem19  12210  ctiunct  12369  ssomct  12374  isstruct2im  12400  isstruct2r  12401  fiinopn  12602  lmfval  12792  upxp  12872  2irrexpqap  13496  dceqnconst  13898  dcapnconst  13899