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  4524  smoeq  6566  tfrlemi1  6608  tfr1onlemaccex  6624  tfrcllemaccex  6637  ereq1  6819  isfsuppfid  7297  updjud  7428  ctssdclemr  7458  tapeq1  7624  tapeq2  7625  elinp  7847  sup3exmid  9295  iccshftr  10412  iccshftl  10414  iccdil  10416  icccntr  10418  fzaddel  10481  elfzomelpfzo  10665  seq3f1olemstep  10971  seq3f1olemp  10972  wrdl1s1  11419  sumeq1  12145  summodclem2  12173  summodc  12174  zsumdc  12175  prodmodclem2  12368  prodmodc  12369  divalglemnn  12709  divalglemeunn  12712  divalglemeuneg  12714  dfgcd2  12815  pythagtriplem18  13088  pythagtriplem19  13089  ctiunct  13388  ssomct  13393  isstruct2im  13419  isstruct2r  13420  ptex  13676  imasmnd2  13817  imasgrp2  13971  isrngd  14358  imasrng  14361  isringd  14452  imasring  14477  subrngpropd  14632  issubrg3  14663  islmod  14735  lmodlema  14736  islmodd  14737  lmodprop2d  14793  fiinopn  15247  lmfval  15436  upxp  15515  ivthdich  15896  2irrexpqap  16231  issubgr  16720  wksfval  16785  iswlk  16786  isclwwlk  16857  clwwlkn1loopb  16883  s2elclwwlknon2  16899  3dom  17240  dceqnconst  17334  dcapnconst  17335