Theorem 3anbi123d 1346

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

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   /\ w3a 1002

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

This theorem depends on definitions:  df-bi 117  df-3an 1004

This theorem is referenced by:  3anbi12d  1347  3anbi13d  1348  3anbi23d  1349  limeq  4468  smoeq  6442  tfrlemi1  6484  tfr1onlemaccex  6500  tfrcllemaccex  6513  ereq1  6695  updjud  7260  ctssdclemr  7290  tapeq1  7449  tapeq2  7450  elinp  7672  sup3exmid  9115  iccshftr  10202  iccshftl  10204  iccdil  10206  icccntr  10208  fzaddel  10267  elfzomelpfzo  10449  seq3f1olemstep  10748  seq3f1olemp  10749  wrdl1s1  11178  sumeq1  11882  summodclem2  11909  summodc  11910  zsumdc  11911  prodmodclem2  12104  prodmodc  12105  divalglemnn  12445  divalglemeunn  12448  divalglemeuneg  12450  dfgcd2  12551  pythagtriplem18  12820  pythagtriplem19  12821  ctiunct  13027  ssomct  13032  isstruct2im  13058  isstruct2r  13059  ptex  13313  imasmnd2  13501  imasgrp2  13663  isrngd  13932  imasrng  13935  isringd  14020  imasring  14043  subrngpropd  14196  issubrg3  14227  islmod  14271  lmodlema  14272  islmodd  14273  lmodprop2d  14328  fiinopn  14694  lmfval  14883  upxp  14962  ivthdich  15343  2irrexpqap  15668  wksfval  16068  iswlk  16069  isclwwlk  16137  clwwlkn1loopb  16162  3dom  16439  dceqnconst  16516  dcapnconst  16517