Theorem 3anbi123d 1353

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  3anbi12d  1354  3anbi13d  1355  3anbi23d  1356  limeq  4522  smoeq  6561  tfrlemi1  6603  tfr1onlemaccex  6619  tfrcllemaccex  6632  ereq1  6814  updjud  7423  ctssdclemr  7453  tapeq1  7619  tapeq2  7620  elinp  7842  sup3exmid  9290  iccshftr  10407  iccshftl  10409  iccdil  10411  icccntr  10413  fzaddel  10476  elfzomelpfzo  10660  seq3f1olemstep  10966  seq3f1olemp  10967  wrdl1s1  11414  sumeq1  12140  summodclem2  12168  summodc  12169  zsumdc  12170  prodmodclem2  12363  prodmodc  12364  divalglemnn  12704  divalglemeunn  12707  divalglemeuneg  12709  dfgcd2  12810  pythagtriplem18  13083  pythagtriplem19  13084  ctiunct  13383  ssomct  13388  isstruct2im  13414  isstruct2r  13415  ptex  13671  imasmnd2  13812  imasgrp2  13966  isrngd  14336  imasrng  14339  isringd  14430  imasring  14453  subrngpropd  14608  issubrg3  14639  islmod  14711  lmodlema  14712  islmodd  14713  lmodprop2d  14769  fiinopn  15196  lmfval  15385  upxp  15464  ivthdich  15845  2irrexpqap  16175  issubgr  16664  wksfval  16729  iswlk  16730  isclwwlk  16801  clwwlkn1loopb  16827  s2elclwwlknon2  16843  3dom  17184  dceqnconst  17277  dcapnconst  17278