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 1088	. 2 ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ ((𝜓 ∧ 𝜃) ∧ 𝜂))
7		df-3an 1088	. 2 ⊢ ((𝜒 ∧ 𝜏 ∧ 𝜁) ↔ ((𝜒 ∧ 𝜏) ∧ 𝜁))
8	5, 6, 7	3bitr4g 314	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ (𝜒 ∧ 𝜏 ∧ 𝜁)))

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

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 1088

This theorem is referenced by:  3anbi12d  1439  3anbi13d  1440  3anbi23d  1441  ax12wdemo  2136  limeq  6332  f13dfv  7231  epne3  7729  oteqimp  7966  xpord2lem  8098  poxp2  8099  xpord3lem  8105  xpord3pred  8108  csbfrecsg  8240  frrlem1  8242  frrlem13  8254  smoeq  8296  on2ind  8610  on3ind  8611  naddasslem1  8635  naddasslem2  8636  naddass  8637  ereq1  8655  sbthfi  9140  indexfi  9287  hartogslem1  9471  brttrcl2  9643  ssttrcl  9644  ttrcltr  9645  ttrclss  9649  ttrclselem2  9655  tz9.1  9658  updjud  9863  alephval3  10039  cofsmo  10198  cfsmolem  10199  alephsing  10205  axdc3lem2  10380  axdc3lem3  10381  axdc3  10383  axdc4lem  10384  zornn0g  10434  fpwwe2lem4  10563  canthwelem  10579  canthwe  10580  pwfseqlem4a  10590  pwfseqlem4  10591  elwina  10615  elina  10616  iswun  10633  elgrug  10721  iccshftr  13423  iccshftl  13425  iccdil  13427  icccntr  13429  fzaddel  13495  elfzomelpfzo  13708  axdc4uzlem  13924  hash3tpb  14436  wrdl1s1  14555  wwlktovf  14898  wwlktovf1  14899  wwlktovfo  14900  wrd2f1tovbij  14902  dfrtrcl2  15004  sqrmo  15193  resqrtcl  15195  resqrtthlem  15196  sqrtneg  15209  sqreu  15303  sqrtthlem  15305  eqsqrtd  15310  prodeq1f  15848  prodeq1  15849  zprod  15879  divalglem10  16348  dfgcd2  16492  coprmprod  16607  pythagtriplem18  16779  pythagtriplem19  16780  prmgaplem3  17000  prmgaplem4  17001  isstruct2  17095  imasval  17450  mreexexlemd  17581  catidd  17617  iscatd2  17618  subsubc  17791  isfunc  17802  funcres2b  17835  ispos  18251  posi  18254  isposd  18259  pospropd  18262  isps  18503  imasmnd2  18677  sgrp2rid2ex  18830  imasgrp2  18963  psgnunilem3  19402  isrngd  20058  imasrng  20062  isringd  20176  imasring  20215  subrngpropd  20453  isdrngd  20650  isdrngdOLD  20652  islmod  20746  lmodlema  20747  islmodd  20748  lmodprop2d  20806  lmhmpropd  20956  isphl  21513  isphld  21539  phlpropd  21540  mdetunilem3  22477  mdetunilem9  22483  fiinopn  22764  iscldtop  22958  lmfval  23095  connsuba  23283  1stcfb  23308  2ndcctbss  23318  subislly  23344  ptval  23433  elpt  23435  elptr  23436  upxp  23486  isfbas  23692  ustval  24066  isust  24067  ustincl  24071  ustdiag  24072  ustinvel  24073  ustexhalf  24074  ust0  24083  imasdsf1olem  24237  tngngp3  24520  lmhmclm  24963  iscph  25046  iscau2  25153  pmltpclem1  25325  isi1f  25551  mbfi1fseqlem6  25597  iblcnlem  25666  dvfsumlem4  25912  aannenlem1  26212  aannenlem2  26213  ulmval  26265  nodense  27580  nosupprefixmo  27588  noinfprefixmo  27589  nosupcbv  27590  nosupfv  27594  noinfcbv  27605  noinffv  27609  noetalem2  27630  eqscut  27693  no2indslem  27837  no3inds  27841  addsproplem3  27854  negsproplem3  27912  mulsproplem10  28004  istrkgb  28358  istrkge  28360  istrkgld  28362  istrkg2ld  28363  istrkg3ld  28364  axtgupdim2  28374  axtgeucl  28375  trgcgrg  28418  ishlg  28505  colline  28552  iscgra  28712  isinag  28741  brbtwn  28802  axpaschlem  28843  axlowdim  28864  axeuclid  28866  eengtrkge  28890  issubgr  29174  nb3grpr  29285  nb3grpr2  29286  cplgr3v  29338  wksfval  29513  iswlk  29514  upgr2wlk  29570  wlkiswwlks2  29778  wwlksnextfun  29801  wwlksnextinj  29802  wwlksnextbij  29805  wwlksnextprop  29815  2wlkdlem4  29831  umgr2wlk  29852  umgrwwlks2on  29860  elwspths2spth  29870  isclwwlk  29886  clwlkclwwlklem1  29901  erclwwlkeq  29920  clwwlkn1loopb  29945  erclwwlkneq  29969  s2elclwwlknon2  30006  3wlkdlem5  30065  3wlkdlem6  30067  3wlkdlem9  30070  3wlkdlem10  30071  uhgr3cyclex  30084  upgr4cycl4dv4e  30087  frgr3v  30177  3cyclfrgrrn1  30187  extwwlkfabel  30255  isplig  30378  lpni  30382  isgrpo  30399  vciOLD  30463  isvclem  30479  isnvlem  30512  sspval  30625  isssp  30626  ajfval  30711  dipdir  30744  siilem2  30754  issh  31110  elunop2  31915  superpos  32256  padct  32616  resspos  32865  isslmd  33128  slmdlema  33129  subsdrg  33221  elrspunidl  33372  constrcbvlem  33718  locfinreflem  33803  locfinref  33804  zarcmplem  33844  zhmnrg  33928  ismntoplly  33988  issiga  34075  isrnsiga  34076  isldsys  34119  rossros  34143  ismeas  34162  isrnmeas  34163  pmeasmono  34288  pmeasadd  34289  istrkg2d  34630  axtgupdim2ALTV  34632  afsval  34635  brafs  34636  bnj919  34730  bnj976  34740  bnj607  34879  bnj873  34887  cvmlift3lem2  35280  cvmlift3lem6  35284  cvmlift3lem7  35285  cvmlift3lem9  35287  cvmlift3  35288  mclsppslem  35543  dfon2lem1  35744  dfon2lem3  35746  dfon2lem7  35750  brofs  35966  ofscom  35968  btwnouttr  35985  brifs  36004  cgr3com  36014  brcolinear  36020  brfs  36040  prodeq12sdv  36179  cbvproddavw2  36257  unblimceq0lem  36467  knoppndvlem21  36493  rdgeqoa  37331  poimirlem4  37591  poimirlem27  37614  mblfinlem3  37626  indexa  37700  sdclem1  37710  fdc  37712  neificl  37720  heiborlem2  37779  isass  37813  ismndo2  37841  isrngo  37864  rngomndo  37902  isgrpda  37922  igenval2  38033  eleqvrels2  38556  eleqvrels3  38557  eqvreleq  38566  lshpset2N  39085  isopos  39146  oposlem  39148  cmtfvalN  39176  cvrfval  39234  3dimlem1  39425  3dim1lem5  39433  lplni2  39504  lvoli2  39548  4atlem11  39576  dalawlem15  39852  cdlemftr3  40532  tendofset  40725  tendoset  40726  istendo  40727  cdlemk28-3  40875  cdlemkid3N  40900  cdlemkid4  40901  lpolsetN  41449  islpolN  41450  lpolconN  41454  isprimroot  42054  aks6d1c1p1  42068  ismrc  42662  rabren3dioph  42776  irrapxlem5  42787  rmydioph  42976  mpaaeu  43112  mpaaval  43113  mpaalem  43114  naddwordnexlem4  43363  dfsucon  43485  minregex  43496  dfrtrcl3  43695  brco3f1o  43995  grumnud  44248  modelaxreplem1  44941  modelaxreplem2  44942  modelaxrep  44944  eliooshift  45477  stoweidlem5  45976  stoweidlem18  45989  stoweidlem28  45999  stoweidlem31  46002  stoweidlem41  46012  stoweidlem43  46014  stoweidlem44  46015  stoweidlem45  46016  stoweidlem51  46022  stoweidlem55  46026  stoweidlem59  46030  issal  46285  fundcmpsurbijinjpreimafv  47381  fundcmpsurbijinj  47384  fundcmpsurinjALT  47386  ichnreuop  47446  proththdlem  47587  6gbe  47745  8gbe  47747  bgoldbtbndlem2  47780  bgoldbtbndlem3  47781  bgoldbtbnd  47783  grtriproplem  47911  grtri  47912  grtrif1o  47914  isgrtri  47915  grimgrtri  47921  usgrexmpl1tri  47989  gpgvtx0  48017  gpgvtx1  48018  gpgedgvtx0  48025  gpgedgvtx1  48026  upwlksfval  48096  isupwlk  48097  el0ldep  48428  ldepspr  48435  lmod1  48454  zlmodzxzldep  48466  catprs  48973  catprsc  48975  prsthinc  49426  2arwcatlem1  49557  cnelsubclem  49565