Theorem 3anbi123d 1294

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 965	. 2 |- ( ( ps /\ th /\ et ) <-> ( ( ps /\ th ) /\ et ) )
7		df-3an 965	. 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 963

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 965

This theorem is referenced by:  3anbi12d  1295  3anbi13d  1296  3anbi23d  1297  limeq  4336  smoeq  6231  tfrlemi1  6273  tfr1onlemaccex  6289  tfrcllemaccex  6302  ereq1  6480  updjud  7016  ctssdclemr  7046  elinp  7377  sup3exmid  8811  iccshftr  9880  iccshftl  9882  iccdil  9884  icccntr  9886  fzaddel  9943  elfzomelpfzo  10112  seq3f1olemstep  10382  seq3f1olemp  10383  sumeq1  11234  summodclem2  11261  summodc  11262  zsumdc  11263  prodmodclem2  11456  prodmodc  11457  divalglemnn  11790  divalglemeunn  11793  divalglemeuneg  11795  dfgcd2  11878  ctiunct  12141  isstruct2im  12160  isstruct2r  12161  fiinopn  12362  lmfval  12552  upxp  12632  2irrexpqap  13255  dceqnconst  13592  dcapnconst  13593