Theorem 3anbi123d 1399

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

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1039

This theorem is referenced by:  3anbi12d  1400  3anbi13d  1401  3anbi23d  1402  ax12wdemo  2012  limeq  5735  f13dfv  6530  epne3  6980  oteqimp  7187  wfrlem1  7414  wfrlem15  7429  smoeq  7447  ereq1  7749  indexfi  8274  hartogslem1  8447  tz9.1  8605  alephval3  8933  cofsmo  9091  cfsmolem  9092  alephsing  9098  axdc3lem2  9273  axdc3lem3  9274  axdc3  9276  axdc4lem  9277  zornn0g  9327  fpwwe2lem5  9456  canthwelem  9472  canthwe  9473  pwfseqlem4a  9483  pwfseqlem4  9484  elwina  9508  elina  9509  iswun  9526  elgrug  9614  iccshftr  12306  iccshftl  12308  iccdil  12310  icccntr  12312  fzaddel  12375  elfzomelpfzo  12572  axdc4uzlem  12782  wrdl1s1  13394  wwlktovf  13699  wwlktovf1  13700  wwlktovfo  13701  wrd2f1tovbij  13703  dfrtrcl2  13802  sqrmo  13992  resqrtcl  13994  resqrtthlem  13995  sqrtneg  14008  sqreu  14100  sqrtthlem  14102  eqsqrtd  14107  prodeq1f  14638  zprod  14667  divalglem10  15125  dfgcd2  15263  coprmprod  15375  pythagtriplem18  15537  pythagtriplem19  15538  prmgaplem3  15757  prmgaplem4  15758  isstruct2  15867  imasval  16171  mreexexlemd  16304  catidd  16341  iscatd2  16342  subsubc  16513  isfunc  16524  funcres2b  16557  ispos  16947  posi  16950  isposd  16955  pospropd  17134  isps  17202  imasmnd2  17327  sgrp2rid2ex  17414  imasgrp2  17530  psgnunilem3  17916  isringd  18585  imasring  18619  isdrngd  18772  islmod  18867  lmodlema  18868  islmodd  18869  lmodprop2d  18925  lmhmpropd  19073  assapropd  19327  isphl  19973  isphld  19999  phlpropd  20000  mdetunilem3  20420  mdetunilem9  20426  fiinopn  20706  iscldtop  20899  lmfval  21036  connsuba  21223  1stcfb  21248  2ndcctbss  21258  subislly  21284  ptval  21373  elpt  21375  elptr  21376  upxp  21426  isfbas  21633  ustval  22006  isust  22007  ustincl  22011  ustdiag  22012  ustinvel  22013  ustexhalf  22014  ust0  22023  imasdsf1olem  22178  tngngp3  22460  lmhmclm  22887  iscph  22970  iscau2  23075  pmltpclem1  23217  isi1f  23441  mbfi1fseqlem6  23487  iblcnlem  23555  dvfsumlem4  23792  aannenlem1  24083  aannenlem2  24084  ulmval  24134  istrkgb  25354  istrkge  25356  istrkgld  25358  istrkg2ld  25359  istrkg3ld  25360  axtgupdim2  25370  axtgeucl  25371  trgcgrg  25410  ishlg  25497  colline  25544  iscgra  25701  isinag  25729  brbtwn  25779  axpaschlem  25820  axlowdim  25841  axeuclid  25843  eengtrkge  25866  issubgr  26163  nb3grpr  26284  nb3grpr2  26285  cplgr3v  26331  wksfval  26505  iswlk  26506  upgr2wlk  26564  wlkiswwlks2  26761  wwlksnextfun  26793  wwlksnextinj  26794  wwlksnextbij  26797  wwlksnextprop  26807  2wlkdlem4  26824  umgr2wlk  26845  umgrwwlks2on  26850  elwspths2spth  26862  isclwwlks  26880  clwlkclwwlklem1  26900  erclwwlkseq  26932  erclwwlksneq  26944  3wlkdlem5  27023  3wlkdlem6  27025  3wlkdlem9  27028  3wlkdlem10  27029  uhgr3cyclex  27042  upgr4cycl4dv4e  27045  frgr3v  27139  3cyclfrgrrn1  27149  numclwlk1lem2foa  27224  numclwlk1lem2f  27225  isplig  27328  lpni  27332  isgrpo  27351  vciOLD  27416  isvclem  27432  isnvlem  27465  sspval  27578  isssp  27579  ajfval  27664  dipdir  27697  siilem2  27707  issh  28065  elunop2  28872  superpos  29213  padct  29497  resspos  29659  isslmd  29755  slmdlema  29756  locfinreflem  29907  locfinref  29908  zhmnrg  30011  ismntoplly  30069  issiga  30174  isrnsigaOLD  30175  isrnsiga  30176  isldsys  30219  rossros  30243  ismeas  30262  isrnmeas  30263  pmeasmono  30386  pmeasadd  30387  istrkg2d  30744  axtgupdim2OLD  30746  afsval  30749  brafs  30750  bnj919  30837  bnj976  30848  bnj607  30986  bnj873  30994  cvmlift3lem2  31302  cvmlift3lem6  31306  cvmlift3lem7  31307  cvmlift3lem9  31309  cvmlift3  31310  mclsppslem  31480  dfon2lem1  31688  dfon2lem3  31690  dfon2lem7  31694  frrlem1  31780  nodense  31842  noprefixmo  31848  nosupfv  31852  noetalem5  31867  noeta  31868  brofs  32112  ofscom  32114  btwnouttr  32131  brifs  32150  cgr3com  32160  brcolinear  32166  brfs  32186  unblimceq0lem  32497  knoppndvlem21  32523  csbwrecsg  33173  rdgeqoa  33218  poimirlem4  33413  poimirlem27  33436  mblfinlem3  33448  indexa  33528  sdclem1  33539  fdc  33541  neificl  33549  heiborlem2  33611  isass  33645  ismndo2  33673  isrngo  33696  rngomndo  33734  isgrpda  33754  igenval2  33865  lshpset2N  34406  isopos  34467  oposlem  34469  cmtfvalN  34497  cvrfval  34555  3dimlem1  34744  3dim1lem5  34752  lplni2  34823  lvoli2  34867  4atlem11  34895  dalawlem15  35171  cdlemftr3  35853  tendofset  36046  tendoset  36047  istendo  36048  cdlemk28-3  36196  cdlemkid3N  36221  cdlemkid4  36222  lpolsetN  36771  islpolN  36772  lpolconN  36776  ismrc  37264  rabren3dioph  37379  irrapxlem5  37390  rmydioph  37581  mpaaeu  37720  mpaaval  37721  mpaalem  37722  dfrtrcl3  38025  brco3f1o  38331  eliooshift  39729  stoweidlem5  40222  stoweidlem18  40235  stoweidlem28  40245  stoweidlem31  40248  stoweidlem41  40258  stoweidlem43  40260  stoweidlem44  40261  stoweidlem45  40262  stoweidlem51  40268  stoweidlem55  40272  stoweidlem59  40276  issal  40534  proththdlem  41530  6gbe  41659  8gbe  41661  bgoldbtbndlem2  41694  bgoldbtbndlem3  41695  bgoldbtbnd  41697  upwlksfval  41716  isupwlk  41717  el0ldep  42255  ldepspr  42262  lmod1  42281  zlmodzxzldep  42293