Theorem 3anbi123d 1438

Description: Deduction joining 3 equivalences to form equivalence of conjunctions. (Contributed by NM, 22-Apr-1994.)

Hypotheses

Ref	Expression
bi3d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
bi3d.2	⊢ (𝜑 → (𝜃 ↔ 𝜏))
bi3d.3	⊢ (𝜑 → (𝜂 ↔ 𝜁))

Assertion

Ref	Expression
3anbi123d	⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ (𝜒 ∧ 𝜏 ∧ 𝜁)))

Proof of Theorem 3anbi123d

Step	Hyp	Ref	Expression
1		bi3d.1	. . . 4 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		bi3d.2	. . . 4 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
3	1, 2	anbi12d 632	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) ↔ (𝜒 ∧ 𝜏)))
4		bi3d.3	. . 3 ⊢ (𝜑 → (𝜂 ↔ 𝜁))
5	3, 4	anbi12d 632	. 2 ⊢ (𝜑 → (((𝜓 ∧ 𝜃) ∧ 𝜂) ↔ ((𝜒 ∧ 𝜏) ∧ 𝜁)))
6		df-3an 1089	. 2 ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ ((𝜓 ∧ 𝜃) ∧ 𝜂))
7		df-3an 1089	. 2 ⊢ ((𝜒 ∧ 𝜏 ∧ 𝜁) ↔ ((𝜒 ∧ 𝜏) ∧ 𝜁))
8	5, 6, 7	3bitr4g 314	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ (𝜒 ∧ 𝜏 ∧ 𝜁)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  3anbi12d  1439  3anbi13d  1440  3anbi23d  1441  ax12wdemo  2135  limeq  6396  f13dfv  7294  epne3  7793  oteqimp  8033  xpord2lem  8167  poxp2  8168  xpord3lem  8174  xpord3pred  8177  csbfrecsg  8309  frrlem1  8311  frrlem13  8323  wfrlem1OLD  8348  wfrlem15OLD  8363  smoeq  8390  on2ind  8707  on3ind  8708  naddasslem1  8732  naddasslem2  8733  naddass  8734  ereq1  8752  sbthfi  9239  indexfi  9400  hartogslem1  9582  brttrcl2  9754  ssttrcl  9755  ttrcltr  9756  ttrclss  9760  ttrclselem2  9766  tz9.1  9769  updjud  9974  alephval3  10150  cofsmo  10309  cfsmolem  10310  alephsing  10316  axdc3lem2  10491  axdc3lem3  10492  axdc3  10494  axdc4lem  10495  zornn0g  10545  fpwwe2lem4  10674  canthwelem  10690  canthwe  10691  pwfseqlem4a  10701  pwfseqlem4  10702  elwina  10726  elina  10727  iswun  10744  elgrug  10832  iccshftr  13526  iccshftl  13528  iccdil  13530  icccntr  13532  fzaddel  13598  elfzomelpfzo  13810  axdc4uzlem  14024  hash3tpb  14534  wrdl1s1  14652  wwlktovf  14995  wwlktovf1  14996  wwlktovfo  14997  wrd2f1tovbij  14999  dfrtrcl2  15101  sqrmo  15290  resqrtcl  15292  resqrtthlem  15293  sqrtneg  15306  sqreu  15399  sqrtthlem  15401  eqsqrtd  15406  prodeq1f  15942  prodeq1  15943  zprod  15973  divalglem10  16439  dfgcd2  16583  coprmprod  16698  pythagtriplem18  16870  pythagtriplem19  16871  prmgaplem3  17091  prmgaplem4  17092  isstruct2  17186  imasval  17556  mreexexlemd  17687  catidd  17723  iscatd2  17724  subsubc  17898  isfunc  17909  funcres2b  17942  ispos  18360  posi  18363  isposd  18368  pospropd  18372  isps  18613  imasmnd2  18787  sgrp2rid2ex  18940  imasgrp2  19073  psgnunilem3  19514  isrngd  20170  imasrng  20174  isringd  20288  imasring  20327  subrngpropd  20568  isdrngd  20765  isdrngdOLD  20767  islmod  20862  lmodlema  20863  islmodd  20864  lmodprop2d  20922  lmhmpropd  21072  isphl  21646  isphld  21672  phlpropd  21673  mdetunilem3  22620  mdetunilem9  22626  fiinopn  22907  iscldtop  23103  lmfval  23240  connsuba  23428  1stcfb  23453  2ndcctbss  23463  subislly  23489  ptval  23578  elpt  23580  elptr  23581  upxp  23631  isfbas  23837  ustval  24211  isust  24212  ustincl  24216  ustdiag  24217  ustinvel  24218  ustexhalf  24219  ust0  24228  imasdsf1olem  24383  tngngp3  24677  lmhmclm  25120  iscph  25204  iscau2  25311  pmltpclem1  25483  isi1f  25709  mbfi1fseqlem6  25755  iblcnlem  25824  dvfsumlem4  26070  aannenlem1  26370  aannenlem2  26371  ulmval  26423  nodense  27737  nosupprefixmo  27745  noinfprefixmo  27746  nosupcbv  27747  nosupfv  27751  noinfcbv  27762  noinffv  27766  noetalem2  27787  eqscut  27850  no2indslem  27987  no3inds  27991  addsproplem3  28004  negsproplem3  28062  mulsproplem10  28151  istrkgb  28463  istrkge  28465  istrkgld  28467  istrkg2ld  28468  istrkg3ld  28469  axtgupdim2  28479  axtgeucl  28480  trgcgrg  28523  ishlg  28610  colline  28657  iscgra  28817  isinag  28846  brbtwn  28914  axpaschlem  28955  axlowdim  28976  axeuclid  28978  eengtrkge  29002  issubgr  29288  nb3grpr  29399  nb3grpr2  29400  cplgr3v  29452  wksfval  29627  iswlk  29628  upgr2wlk  29686  wlkiswwlks2  29895  wwlksnextfun  29918  wwlksnextinj  29919  wwlksnextbij  29922  wwlksnextprop  29932  2wlkdlem4  29948  umgr2wlk  29969  umgrwwlks2on  29977  elwspths2spth  29987  isclwwlk  30003  clwlkclwwlklem1  30018  erclwwlkeq  30037  clwwlkn1loopb  30062  erclwwlkneq  30086  s2elclwwlknon2  30123  3wlkdlem5  30182  3wlkdlem6  30184  3wlkdlem9  30187  3wlkdlem10  30188  uhgr3cyclex  30201  upgr4cycl4dv4e  30204  frgr3v  30294  3cyclfrgrrn1  30304  extwwlkfabel  30372  isplig  30495  lpni  30499  isgrpo  30516  vciOLD  30580  isvclem  30596  isnvlem  30629  sspval  30742  isssp  30743  ajfval  30828  dipdir  30861  siilem2  30871  issh  31227  elunop2  32032  superpos  32373  padct  32731  resspos  32956  isslmd  33208  slmdlema  33209  elrspunidl  33456  locfinreflem  33839  locfinref  33840  zarcmplem  33880  zhmnrg  33966  ismntoplly  34026  issiga  34113  isrnsiga  34114  isldsys  34157  rossros  34181  ismeas  34200  isrnmeas  34201  pmeasmono  34326  pmeasadd  34327  istrkg2d  34681  axtgupdim2ALTV  34683  afsval  34686  brafs  34687  bnj919  34781  bnj976  34791  bnj607  34930  bnj873  34938  cvmlift3lem2  35325  cvmlift3lem6  35329  cvmlift3lem7  35330  cvmlift3lem9  35332  cvmlift3  35333  mclsppslem  35588  dfon2lem1  35784  dfon2lem3  35786  dfon2lem7  35790  brofs  36006  ofscom  36008  btwnouttr  36025  brifs  36044  cgr3com  36054  brcolinear  36060  brfs  36080  prodeq12sdv  36219  cbvproddavw2  36297  unblimceq0lem  36507  knoppndvlem21  36533  rdgeqoa  37371  poimirlem4  37631  poimirlem27  37654  mblfinlem3  37666  indexa  37740  sdclem1  37750  fdc  37752  neificl  37760  heiborlem2  37819  isass  37853  ismndo2  37881  isrngo  37904  rngomndo  37942  isgrpda  37962  igenval2  38073  eleqvrels2  38593  eleqvrels3  38594  eqvreleq  38603  lshpset2N  39120  isopos  39181  oposlem  39183  cmtfvalN  39211  cvrfval  39269  3dimlem1  39460  3dim1lem5  39468  lplni2  39539  lvoli2  39583  4atlem11  39611  dalawlem15  39887  cdlemftr3  40567  tendofset  40760  tendoset  40761  istendo  40762  cdlemk28-3  40910  cdlemkid3N  40935  cdlemkid4  40936  lpolsetN  41484  islpolN  41485  lpolconN  41489  isprimroot  42094  aks6d1c1p1  42108  ismrc  42712  rabren3dioph  42826  irrapxlem5  42837  rmydioph  43026  mpaaeu  43162  mpaaval  43163  mpaalem  43164  naddwordnexlem4  43414  dfsucon  43536  minregex  43547  dfrtrcl3  43746  brco3f1o  44046  grumnud  44305  modelaxreplem1  44995  modelaxreplem2  44996  modelaxrep  44998  eliooshift  45519  stoweidlem5  46020  stoweidlem18  46033  stoweidlem28  46043  stoweidlem31  46046  stoweidlem41  46056  stoweidlem43  46058  stoweidlem44  46059  stoweidlem45  46060  stoweidlem51  46066  stoweidlem55  46070  stoweidlem59  46074  issal  46329  fundcmpsurbijinjpreimafv  47394  fundcmpsurbijinj  47397  fundcmpsurinjALT  47399  ichnreuop  47459  proththdlem  47600  6gbe  47758  8gbe  47760  bgoldbtbndlem2  47793  bgoldbtbndlem3  47794  bgoldbtbnd  47796  grtriproplem  47906  grtri  47907  grtrif1o  47909  isgrtri  47910  grimgrtri  47916  usgrexmpl1tri  47984  gpgvtx0  48008  gpgvtx1  48009  gpgedgvtx0  48019  gpgedgvtx1  48020  upwlksfval  48051  isupwlk  48052  el0ldep  48383  ldepspr  48390  lmod1  48409  zlmodzxzldep  48421  catprs  48900  catprsc  48902  prsthinc  49111