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  2135  limeq  6364  f13dfv  7266  epne3  7765  oteqimp  8005  xpord2lem  8139  poxp2  8140  xpord3lem  8146  xpord3pred  8149  csbfrecsg  8281  frrlem1  8283  frrlem13  8295  wfrlem1OLD  8320  wfrlem15OLD  8335  smoeq  8362  on2ind  8679  on3ind  8680  naddasslem1  8704  naddasslem2  8705  naddass  8706  ereq1  8724  sbthfi  9211  indexfi  9370  hartogslem1  9554  brttrcl2  9726  ssttrcl  9727  ttrcltr  9728  ttrclss  9732  ttrclselem2  9738  tz9.1  9741  updjud  9946  alephval3  10122  cofsmo  10281  cfsmolem  10282  alephsing  10288  axdc3lem2  10463  axdc3lem3  10464  axdc3  10466  axdc4lem  10467  zornn0g  10517  fpwwe2lem4  10646  canthwelem  10662  canthwe  10663  pwfseqlem4a  10673  pwfseqlem4  10674  elwina  10698  elina  10699  iswun  10716  elgrug  10804  iccshftr  13501  iccshftl  13503  iccdil  13505  icccntr  13507  fzaddel  13573  elfzomelpfzo  13785  axdc4uzlem  13999  hash3tpb  14511  wrdl1s1  14630  wwlktovf  14973  wwlktovf1  14974  wwlktovfo  14975  wrd2f1tovbij  14977  dfrtrcl2  15079  sqrmo  15268  resqrtcl  15270  resqrtthlem  15271  sqrtneg  15284  sqreu  15377  sqrtthlem  15379  eqsqrtd  15384  prodeq1f  15920  prodeq1  15921  zprod  15951  divalglem10  16419  dfgcd2  16563  coprmprod  16678  pythagtriplem18  16850  pythagtriplem19  16851  prmgaplem3  17071  prmgaplem4  17072  isstruct2  17166  imasval  17523  mreexexlemd  17654  catidd  17690  iscatd2  17691  subsubc  17864  isfunc  17875  funcres2b  17908  ispos  18324  posi  18327  isposd  18332  pospropd  18335  isps  18576  imasmnd2  18750  sgrp2rid2ex  18903  imasgrp2  19036  psgnunilem3  19475  isrngd  20131  imasrng  20135  isringd  20249  imasring  20288  subrngpropd  20526  isdrngd  20723  isdrngdOLD  20725  islmod  20819  lmodlema  20820  islmodd  20821  lmodprop2d  20879  lmhmpropd  21029  isphl  21586  isphld  21612  phlpropd  21613  mdetunilem3  22550  mdetunilem9  22556  fiinopn  22837  iscldtop  23031  lmfval  23168  connsuba  23356  1stcfb  23381  2ndcctbss  23391  subislly  23417  ptval  23506  elpt  23508  elptr  23509  upxp  23559  isfbas  23765  ustval  24139  isust  24140  ustincl  24144  ustdiag  24145  ustinvel  24146  ustexhalf  24147  ust0  24156  imasdsf1olem  24310  tngngp3  24593  lmhmclm  25036  iscph  25120  iscau2  25227  pmltpclem1  25399  isi1f  25625  mbfi1fseqlem6  25671  iblcnlem  25740  dvfsumlem4  25986  aannenlem1  26286  aannenlem2  26287  ulmval  26339  nodense  27654  nosupprefixmo  27662  noinfprefixmo  27663  nosupcbv  27664  nosupfv  27668  noinfcbv  27679  noinffv  27683  noetalem2  27704  eqscut  27767  no2indslem  27904  no3inds  27908  addsproplem3  27921  negsproplem3  27979  mulsproplem10  28068  istrkgb  28380  istrkge  28382  istrkgld  28384  istrkg2ld  28385  istrkg3ld  28386  axtgupdim2  28396  axtgeucl  28397  trgcgrg  28440  ishlg  28527  colline  28574  iscgra  28734  isinag  28763  brbtwn  28824  axpaschlem  28865  axlowdim  28886  axeuclid  28888  eengtrkge  28912  issubgr  29196  nb3grpr  29307  nb3grpr2  29308  cplgr3v  29360  wksfval  29535  iswlk  29536  upgr2wlk  29594  wlkiswwlks2  29803  wwlksnextfun  29826  wwlksnextinj  29827  wwlksnextbij  29830  wwlksnextprop  29840  2wlkdlem4  29856  umgr2wlk  29877  umgrwwlks2on  29885  elwspths2spth  29895  isclwwlk  29911  clwlkclwwlklem1  29926  erclwwlkeq  29945  clwwlkn1loopb  29970  erclwwlkneq  29994  s2elclwwlknon2  30031  3wlkdlem5  30090  3wlkdlem6  30092  3wlkdlem9  30095  3wlkdlem10  30096  uhgr3cyclex  30109  upgr4cycl4dv4e  30112  frgr3v  30202  3cyclfrgrrn1  30212  extwwlkfabel  30280  isplig  30403  lpni  30407  isgrpo  30424  vciOLD  30488  isvclem  30504  isnvlem  30537  sspval  30650  isssp  30651  ajfval  30736  dipdir  30769  siilem2  30779  issh  31135  elunop2  31940  superpos  32281  padct  32643  resspos  32892  isslmd  33145  slmdlema  33146  subsdrg  33238  elrspunidl  33389  constrcbvlem  33735  locfinreflem  33817  locfinref  33818  zarcmplem  33858  zhmnrg  33942  ismntoplly  34002  issiga  34089  isrnsiga  34090  isldsys  34133  rossros  34157  ismeas  34176  isrnmeas  34177  pmeasmono  34302  pmeasadd  34303  istrkg2d  34644  axtgupdim2ALTV  34646  afsval  34649  brafs  34650  bnj919  34744  bnj976  34754  bnj607  34893  bnj873  34901  cvmlift3lem2  35288  cvmlift3lem6  35292  cvmlift3lem7  35293  cvmlift3lem9  35295  cvmlift3  35296  mclsppslem  35551  dfon2lem1  35747  dfon2lem3  35749  dfon2lem7  35753  brofs  35969  ofscom  35971  btwnouttr  35988  brifs  36007  cgr3com  36017  brcolinear  36023  brfs  36043  prodeq12sdv  36182  cbvproddavw2  36260  unblimceq0lem  36470  knoppndvlem21  36496  rdgeqoa  37334  poimirlem4  37594  poimirlem27  37617  mblfinlem3  37629  indexa  37703  sdclem1  37713  fdc  37715  neificl  37723  heiborlem2  37782  isass  37816  ismndo2  37844  isrngo  37867  rngomndo  37905  isgrpda  37925  igenval2  38036  eleqvrels2  38556  eleqvrels3  38557  eqvreleq  38566  lshpset2N  39083  isopos  39144  oposlem  39146  cmtfvalN  39174  cvrfval  39232  3dimlem1  39423  3dim1lem5  39431  lplni2  39502  lvoli2  39546  4atlem11  39574  dalawlem15  39850  cdlemftr3  40530  tendofset  40723  tendoset  40724  istendo  40725  cdlemk28-3  40873  cdlemkid3N  40898  cdlemkid4  40899  lpolsetN  41447  islpolN  41448  lpolconN  41452  isprimroot  42052  aks6d1c1p1  42066  ismrc  42671  rabren3dioph  42785  irrapxlem5  42796  rmydioph  42985  mpaaeu  43121  mpaaval  43122  mpaalem  43123  naddwordnexlem4  43372  dfsucon  43494  minregex  43505  dfrtrcl3  43704  brco3f1o  44004  grumnud  44258  modelaxreplem1  44951  modelaxreplem2  44952  modelaxrep  44954  eliooshift  45483  stoweidlem5  45982  stoweidlem18  45995  stoweidlem28  46005  stoweidlem31  46008  stoweidlem41  46018  stoweidlem43  46020  stoweidlem44  46021  stoweidlem45  46022  stoweidlem51  46028  stoweidlem55  46032  stoweidlem59  46036  issal  46291  fundcmpsurbijinjpreimafv  47369  fundcmpsurbijinj  47372  fundcmpsurinjALT  47374  ichnreuop  47434  proththdlem  47575  6gbe  47733  8gbe  47735  bgoldbtbndlem2  47768  bgoldbtbndlem3  47769  bgoldbtbnd  47771  grtriproplem  47899  grtri  47900  grtrif1o  47902  isgrtri  47903  grimgrtri  47909  usgrexmpl1tri  47977  gpgvtx0  48005  gpgvtx1  48006  gpgedgvtx0  48013  gpgedgvtx1  48014  upwlksfval  48058  isupwlk  48059  el0ldep  48390  ldepspr  48397  lmod1  48416  zlmodzxzldep  48428  catprs  48934  catprsc  48936  prsthinc  49298  2arwcatlem1  49420  cnelsubclem  49428