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  6347  f13dfv  7252  epne3  7752  oteqimp  7990  xpord2lem  8124  poxp2  8125  xpord3lem  8131  xpord3pred  8134  csbfrecsg  8266  frrlem1  8268  frrlem13  8280  smoeq  8322  on2ind  8636  on3ind  8637  naddasslem1  8661  naddasslem2  8662  naddass  8663  ereq1  8681  sbthfi  9169  indexfi  9318  hartogslem1  9502  brttrcl2  9674  ssttrcl  9675  ttrcltr  9676  ttrclss  9680  ttrclselem2  9686  tz9.1  9689  updjud  9894  alephval3  10070  cofsmo  10229  cfsmolem  10230  alephsing  10236  axdc3lem2  10411  axdc3lem3  10412  axdc3  10414  axdc4lem  10415  zornn0g  10465  fpwwe2lem4  10594  canthwelem  10610  canthwe  10611  pwfseqlem4a  10621  pwfseqlem4  10622  elwina  10646  elina  10647  iswun  10664  elgrug  10752  iccshftr  13454  iccshftl  13456  iccdil  13458  icccntr  13460  fzaddel  13526  elfzomelpfzo  13739  axdc4uzlem  13955  hash3tpb  14467  wrdl1s1  14586  wwlktovf  14929  wwlktovf1  14930  wwlktovfo  14931  wrd2f1tovbij  14933  dfrtrcl2  15035  sqrmo  15224  resqrtcl  15226  resqrtthlem  15227  sqrtneg  15240  sqreu  15334  sqrtthlem  15336  eqsqrtd  15341  prodeq1f  15879  prodeq1  15880  zprod  15910  divalglem10  16379  dfgcd2  16523  coprmprod  16638  pythagtriplem18  16810  pythagtriplem19  16811  prmgaplem3  17031  prmgaplem4  17032  isstruct2  17126  imasval  17481  mreexexlemd  17612  catidd  17648  iscatd2  17649  subsubc  17822  isfunc  17833  funcres2b  17866  ispos  18282  posi  18285  isposd  18290  pospropd  18293  isps  18534  imasmnd2  18708  sgrp2rid2ex  18861  imasgrp2  18994  psgnunilem3  19433  isrngd  20089  imasrng  20093  isringd  20207  imasring  20246  subrngpropd  20484  isdrngd  20681  isdrngdOLD  20683  islmod  20777  lmodlema  20778  islmodd  20779  lmodprop2d  20837  lmhmpropd  20987  isphl  21544  isphld  21570  phlpropd  21571  mdetunilem3  22508  mdetunilem9  22514  fiinopn  22795  iscldtop  22989  lmfval  23126  connsuba  23314  1stcfb  23339  2ndcctbss  23349  subislly  23375  ptval  23464  elpt  23466  elptr  23467  upxp  23517  isfbas  23723  ustval  24097  isust  24098  ustincl  24102  ustdiag  24103  ustinvel  24104  ustexhalf  24105  ust0  24114  imasdsf1olem  24268  tngngp3  24551  lmhmclm  24994  iscph  25077  iscau2  25184  pmltpclem1  25356  isi1f  25582  mbfi1fseqlem6  25628  iblcnlem  25697  dvfsumlem4  25943  aannenlem1  26243  aannenlem2  26244  ulmval  26296  nodense  27611  nosupprefixmo  27619  noinfprefixmo  27620  nosupcbv  27621  nosupfv  27625  noinfcbv  27636  noinffv  27640  noetalem2  27661  eqscut  27724  no2indslem  27868  no3inds  27872  addsproplem3  27885  negsproplem3  27943  mulsproplem10  28035  istrkgb  28389  istrkge  28391  istrkgld  28393  istrkg2ld  28394  istrkg3ld  28395  axtgupdim2  28405  axtgeucl  28406  trgcgrg  28449  ishlg  28536  colline  28583  iscgra  28743  isinag  28772  brbtwn  28833  axpaschlem  28874  axlowdim  28895  axeuclid  28897  eengtrkge  28921  issubgr  29205  nb3grpr  29316  nb3grpr2  29317  cplgr3v  29369  wksfval  29544  iswlk  29545  upgr2wlk  29603  wlkiswwlks2  29812  wwlksnextfun  29835  wwlksnextinj  29836  wwlksnextbij  29839  wwlksnextprop  29849  2wlkdlem4  29865  umgr2wlk  29886  umgrwwlks2on  29894  elwspths2spth  29904  isclwwlk  29920  clwlkclwwlklem1  29935  erclwwlkeq  29954  clwwlkn1loopb  29979  erclwwlkneq  30003  s2elclwwlknon2  30040  3wlkdlem5  30099  3wlkdlem6  30101  3wlkdlem9  30104  3wlkdlem10  30105  uhgr3cyclex  30118  upgr4cycl4dv4e  30121  frgr3v  30211  3cyclfrgrrn1  30221  extwwlkfabel  30289  isplig  30412  lpni  30416  isgrpo  30433  vciOLD  30497  isvclem  30513  isnvlem  30546  sspval  30659  isssp  30660  ajfval  30745  dipdir  30778  siilem2  30788  issh  31144  elunop2  31949  superpos  32290  padct  32650  resspos  32899  isslmd  33162  slmdlema  33163  subsdrg  33255  elrspunidl  33406  constrcbvlem  33752  locfinreflem  33837  locfinref  33838  zarcmplem  33878  zhmnrg  33962  ismntoplly  34022  issiga  34109  isrnsiga  34110  isldsys  34153  rossros  34177  ismeas  34196  isrnmeas  34197  pmeasmono  34322  pmeasadd  34323  istrkg2d  34664  axtgupdim2ALTV  34666  afsval  34669  brafs  34670  bnj919  34764  bnj976  34774  bnj607  34913  bnj873  34921  cvmlift3lem2  35314  cvmlift3lem6  35318  cvmlift3lem7  35319  cvmlift3lem9  35321  cvmlift3  35322  mclsppslem  35577  dfon2lem1  35778  dfon2lem3  35780  dfon2lem7  35784  brofs  36000  ofscom  36002  btwnouttr  36019  brifs  36038  cgr3com  36048  brcolinear  36054  brfs  36074  prodeq12sdv  36213  cbvproddavw2  36291  unblimceq0lem  36501  knoppndvlem21  36527  rdgeqoa  37365  poimirlem4  37625  poimirlem27  37648  mblfinlem3  37660  indexa  37734  sdclem1  37744  fdc  37746  neificl  37754  heiborlem2  37813  isass  37847  ismndo2  37875  isrngo  37898  rngomndo  37936  isgrpda  37956  igenval2  38067  eleqvrels2  38590  eleqvrels3  38591  eqvreleq  38600  lshpset2N  39119  isopos  39180  oposlem  39182  cmtfvalN  39210  cvrfval  39268  3dimlem1  39459  3dim1lem5  39467  lplni2  39538  lvoli2  39582  4atlem11  39610  dalawlem15  39886  cdlemftr3  40566  tendofset  40759  tendoset  40760  istendo  40761  cdlemk28-3  40909  cdlemkid3N  40934  cdlemkid4  40935  lpolsetN  41483  islpolN  41484  lpolconN  41488  isprimroot  42088  aks6d1c1p1  42102  ismrc  42696  rabren3dioph  42810  irrapxlem5  42821  rmydioph  43010  mpaaeu  43146  mpaaval  43147  mpaalem  43148  naddwordnexlem4  43397  dfsucon  43519  minregex  43530  dfrtrcl3  43729  brco3f1o  44029  grumnud  44282  modelaxreplem1  44975  modelaxreplem2  44976  modelaxrep  44978  eliooshift  45511  stoweidlem5  46010  stoweidlem18  46023  stoweidlem28  46033  stoweidlem31  46036  stoweidlem41  46046  stoweidlem43  46048  stoweidlem44  46049  stoweidlem45  46050  stoweidlem51  46056  stoweidlem55  46060  stoweidlem59  46064  issal  46319  fundcmpsurbijinjpreimafv  47412  fundcmpsurbijinj  47415  fundcmpsurinjALT  47417  ichnreuop  47477  proththdlem  47618  6gbe  47776  8gbe  47778  bgoldbtbndlem2  47811  bgoldbtbndlem3  47812  bgoldbtbnd  47814  grtriproplem  47942  grtri  47943  grtrif1o  47945  isgrtri  47946  grimgrtri  47952  usgrexmpl1tri  48020  gpgvtx0  48048  gpgvtx1  48049  gpgedgvtx0  48056  gpgedgvtx1  48057  upwlksfval  48127  isupwlk  48128  el0ldep  48459  ldepspr  48466  lmod1  48485  zlmodzxzldep  48497  catprs  49004  catprsc  49006  prsthinc  49457  2arwcatlem1  49588  cnelsubclem  49596