Theorem 3anbi123d 1435

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  1436  3anbi13d  1437  3anbi23d  1438  ax12wdemo  2132  limeq  6397  f13dfv  7293  epne3  7791  oteqimp  8031  xpord2lem  8165  poxp2  8166  xpord3lem  8172  xpord3pred  8175  csbfrecsg  8307  frrlem1  8309  frrlem13  8321  wfrlem1OLD  8346  wfrlem15OLD  8361  smoeq  8388  on2ind  8705  on3ind  8706  naddasslem1  8730  naddasslem2  8731  naddass  8732  ereq1  8750  sbthfi  9236  indexfi  9397  hartogslem1  9579  brttrcl2  9751  ssttrcl  9752  ttrcltr  9753  ttrclss  9757  ttrclselem2  9763  tz9.1  9766  updjud  9971  alephval3  10147  cofsmo  10306  cfsmolem  10307  alephsing  10313  axdc3lem2  10488  axdc3lem3  10489  axdc3  10491  axdc4lem  10492  zornn0g  10542  fpwwe2lem4  10671  canthwelem  10687  canthwe  10688  pwfseqlem4a  10698  pwfseqlem4  10699  elwina  10723  elina  10724  iswun  10741  elgrug  10829  iccshftr  13522  iccshftl  13524  iccdil  13526  icccntr  13528  fzaddel  13594  elfzomelpfzo  13806  axdc4uzlem  14020  hash3tpb  14530  wrdl1s1  14648  wwlktovf  14991  wwlktovf1  14992  wwlktovfo  14993  wrd2f1tovbij  14995  dfrtrcl2  15097  sqrmo  15286  resqrtcl  15288  resqrtthlem  15289  sqrtneg  15302  sqreu  15395  sqrtthlem  15397  eqsqrtd  15402  prodeq1f  15938  prodeq1  15939  zprod  15969  divalglem10  16435  dfgcd2  16579  coprmprod  16694  pythagtriplem18  16865  pythagtriplem19  16866  prmgaplem3  17086  prmgaplem4  17087  isstruct2  17182  imasval  17557  mreexexlemd  17688  catidd  17724  iscatd2  17725  subsubc  17903  isfunc  17914  funcres2b  17947  ispos  18371  posi  18374  isposd  18380  pospropd  18384  isps  18625  imasmnd2  18799  sgrp2rid2ex  18952  imasgrp2  19085  psgnunilem3  19528  isrngd  20190  imasrng  20194  isringd  20304  imasring  20343  subrngpropd  20584  isdrngd  20781  isdrngdOLD  20783  islmod  20878  lmodlema  20879  islmodd  20880  lmodprop2d  20938  lmhmpropd  21089  isphl  21663  isphld  21689  phlpropd  21690  mdetunilem3  22635  mdetunilem9  22641  fiinopn  22922  iscldtop  23118  lmfval  23255  connsuba  23443  1stcfb  23468  2ndcctbss  23478  subislly  23504  ptval  23593  elpt  23595  elptr  23596  upxp  23646  isfbas  23852  ustval  24226  isust  24227  ustincl  24231  ustdiag  24232  ustinvel  24233  ustexhalf  24234  ust0  24243  imasdsf1olem  24398  tngngp3  24692  lmhmclm  25133  iscph  25217  iscau2  25324  pmltpclem1  25496  isi1f  25722  mbfi1fseqlem6  25769  iblcnlem  25838  dvfsumlem4  26084  aannenlem1  26384  aannenlem2  26385  ulmval  26437  nodense  27751  nosupprefixmo  27759  noinfprefixmo  27760  nosupcbv  27761  nosupfv  27765  noinfcbv  27776  noinffv  27780  noetalem2  27801  eqscut  27864  no2indslem  28001  no3inds  28005  addsproplem3  28018  negsproplem3  28076  mulsproplem10  28165  istrkgb  28477  istrkge  28479  istrkgld  28481  istrkg2ld  28482  istrkg3ld  28483  axtgupdim2  28493  axtgeucl  28494  trgcgrg  28537  ishlg  28624  colline  28671  iscgra  28831  isinag  28860  brbtwn  28928  axpaschlem  28969  axlowdim  28990  axeuclid  28992  eengtrkge  29016  issubgr  29302  nb3grpr  29413  nb3grpr2  29414  cplgr3v  29466  wksfval  29641  iswlk  29642  upgr2wlk  29700  wlkiswwlks2  29904  wwlksnextfun  29927  wwlksnextinj  29928  wwlksnextbij  29931  wwlksnextprop  29941  2wlkdlem4  29957  umgr2wlk  29978  umgrwwlks2on  29986  elwspths2spth  29996  isclwwlk  30012  clwlkclwwlklem1  30027  erclwwlkeq  30046  clwwlkn1loopb  30071  erclwwlkneq  30095  s2elclwwlknon2  30132  3wlkdlem5  30191  3wlkdlem6  30193  3wlkdlem9  30196  3wlkdlem10  30197  uhgr3cyclex  30210  upgr4cycl4dv4e  30213  frgr3v  30303  3cyclfrgrrn1  30313  extwwlkfabel  30381  isplig  30504  lpni  30508  isgrpo  30525  vciOLD  30589  isvclem  30605  isnvlem  30638  sspval  30751  isssp  30752  ajfval  30837  dipdir  30870  siilem2  30880  issh  31236  elunop2  32041  superpos  32382  padct  32736  resspos  32940  isslmd  33190  slmdlema  33191  elrspunidl  33435  locfinreflem  33800  locfinref  33801  zarcmplem  33841  zhmnrg  33927  ismntoplly  33987  issiga  34092  isrnsiga  34093  isldsys  34136  rossros  34160  ismeas  34179  isrnmeas  34180  pmeasmono  34305  pmeasadd  34306  istrkg2d  34659  axtgupdim2ALTV  34661  afsval  34664  brafs  34665  bnj919  34759  bnj976  34769  bnj607  34908  bnj873  34916  cvmlift3lem2  35304  cvmlift3lem6  35308  cvmlift3lem7  35309  cvmlift3lem9  35311  cvmlift3  35312  mclsppslem  35567  dfon2lem1  35764  dfon2lem3  35766  dfon2lem7  35770  brofs  35986  ofscom  35988  btwnouttr  36005  brifs  36024  cgr3com  36034  brcolinear  36040  brfs  36060  prodeq12sdv  36200  cbvproddavw2  36278  unblimceq0lem  36488  knoppndvlem21  36514  rdgeqoa  37352  poimirlem4  37610  poimirlem27  37633  mblfinlem3  37645  indexa  37719  sdclem1  37729  fdc  37731  neificl  37739  heiborlem2  37798  isass  37832  ismndo2  37860  isrngo  37883  rngomndo  37921  isgrpda  37941  igenval2  38052  eleqvrels2  38573  eleqvrels3  38574  eqvreleq  38583  lshpset2N  39100  isopos  39161  oposlem  39163  cmtfvalN  39191  cvrfval  39249  3dimlem1  39440  3dim1lem5  39448  lplni2  39519  lvoli2  39563  4atlem11  39591  dalawlem15  39867  cdlemftr3  40547  tendofset  40740  tendoset  40741  istendo  40742  cdlemk28-3  40890  cdlemkid3N  40915  cdlemkid4  40916  lpolsetN  41464  islpolN  41465  lpolconN  41469  isprimroot  42074  aks6d1c1p1  42088  ismrc  42688  rabren3dioph  42802  irrapxlem5  42813  rmydioph  43002  mpaaeu  43138  mpaaval  43139  mpaalem  43140  naddwordnexlem4  43390  dfsucon  43512  minregex  43523  dfrtrcl3  43722  brco3f1o  44022  grumnud  44281  modelaxreplem1  44942  modelaxreplem2  44943  modelaxrep  44945  eliooshift  45458  stoweidlem5  45960  stoweidlem18  45973  stoweidlem28  45983  stoweidlem31  45986  stoweidlem41  45996  stoweidlem43  45998  stoweidlem44  45999  stoweidlem45  46000  stoweidlem51  46006  stoweidlem55  46010  stoweidlem59  46014  issal  46269  fundcmpsurbijinjpreimafv  47331  fundcmpsurbijinj  47334  fundcmpsurinjALT  47336  ichnreuop  47396  proththdlem  47537  6gbe  47695  8gbe  47697  bgoldbtbndlem2  47730  bgoldbtbndlem3  47731  bgoldbtbnd  47733  grtriproplem  47843  grtri  47844  grtrif1o  47846  isgrtri  47847  grimgrtri  47851  usgrexmpl1tri  47919  gpgvtx0  47943  gpgvtx1  47944  gpgedgvtx0  47953  gpgedgvtx1  47954  upwlksfval  47978  isupwlk  47979  el0ldep  48311  ldepspr  48318  lmod1  48337  zlmodzxzldep  48349  catprs  48799  catprsc  48801  prsthinc  48854