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  7422  ctssdclemr  7452  tapeq1  7618  tapeq2  7619  elinp  7841  sup3exmid  9287  iccshftr  10396  iccshftl  10398  iccdil  10400  icccntr  10402  fzaddel  10465  elfzomelpfzo  10649  seq3f1olemstep  10951  seq3f1olemp  10952  wrdl1s1  11398  sumeq1  12121  summodclem2  12149  summodc  12150  zsumdc  12151  prodmodclem2  12344  prodmodc  12345  divalglemnn  12685  divalglemeunn  12688  divalglemeuneg  12690  dfgcd2  12791  pythagtriplem18  13060  pythagtriplem19  13061  ctiunct  13331  ssomct  13336  isstruct2im  13362  isstruct2r  13363  ptex  13618  imasmnd2  13759  imasgrp2  13913  isrngd  14252  imasrng  14255  isringd  14346  imasring  14369  subrngpropd  14524  issubrg3  14555  islmod  14627  lmodlema  14628  islmodd  14629  lmodprop2d  14685  fiinopn  15105  lmfval  15294  upxp  15373  ivthdich  15754  2irrexpqap  16080  issubgr  16498  wksfval  16563  iswlk  16564  isclwwlk  16635  clwwlkn1loopb  16661  s2elclwwlknon2  16677  3dom  17018  dceqnconst  17110  dcapnconst  17111