Theorem 3anbi123d 1462

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  3anbi12d  1463  3anbi13d  1464  3anbi23d  1465  ax12wdemo  2176  limeq  6370  f13dfv  7270  epne3  7768  oteqimp  8001  xpord2lem  8134  poxp2  8135  xpord3lem  8141  xpord3pred  8144  csbfrecsg  8277  frrlem1  8279  frrlem13  8291  smoeq  8333  on2ind  8651  on3ind  8652  naddasslem1  8677  naddasslem2  8678  naddass  8679  ereq1  8698  sbthfi  9179  indexfi  9313  hartogslem1  9500  brttrcl2  9679  ssttrcl  9680  ttrcltr  9681  ttrclss  9685  ttrclselem2  9691  tz9.1  9694  updjud  9916  alephval3  10090  cofsmo  10249  cfsmolem  10250  alephsing  10256  axdc3lem2  10431  axdc3lem3  10432  axdc3  10434  axdc4lem  10435  zornn0g  10485  fpwwe2lem4  10615  canthwelem  10631  canthwe  10632  pwfseqlem4a  10642  pwfseqlem4  10643  elwina  10667  elina  10668  iswun  10685  elgrug  10773  iccshftr  13509  iccshftl  13511  iccdil  13513  icccntr  13515  fzaddel  13582  elfzomelpfzo  13797  axdc4uzlem  14015  hash3tpb  14528  wrdl1s1  14648  wwlktovf  14989  wwlktovf1  14990  wwlktovfo  14991  wrd2f1tovbij  14993  dfrtrcl2  15095  sqrmo  15298  resqrtcl  15300  resqrtthlem  15301  sqrtneg  15314  sqreu  15408  sqrtthlem  15410  eqsqrtd  15415  prodeq1f  15956  prodeq1  15957  zprod  15987  divalglem10  16456  dfgcd2  16600  coprmprod  16715  pythagtriplem18  16888  pythagtriplem19  16889  prmgaplem3  17109  prmgaplem4  17110  isstruct2  17205  imasval  17561  mreexexlemd  17696  catidd  17732  iscatd2  17733  subsubc  17906  isfunc  17917  funcres2b  17950  ispos  18366  posi  18369  isposd  18374  pospropd  18377  resspos  18481  isps  18620  imasmnd2  18828  sgrp2rid2ex  18985  imasgrp2  19117  psgnunilem3  19562  isrngd  20247  imasrng  20251  isringd  20370  imasring  20408  subrngpropd  20649  isdrngd  20843  isdrngdOLD  20845  islmod  20959  lmodlema  20960  islmodd  20961  lmodprop2d  21019  lmhmpropd  21168  isphl  21743  isphld  21769  phlpropd  21770  mdetunilem3  22736  mdetunilem9  22742  fiinopn  23023  iscldtop  23217  lmfval  23354  connsuba  23542  1stcfb  23567  2ndcctbss  23577  subislly  23603  ptval  23692  elpt  23694  elptr  23695  upxp  23745  isfbas  23951  ustval  24325  isust  24326  ustincl  24330  ustdiag  24331  ustinvel  24332  ustexhalf  24333  ust0  24342  imasdsf1olem  24495  tngngp3  24778  lmhmclm  25211  iscph  25294  iscau2  25401  pmltpclem1  25572  isi1f  25798  mbfi1fseqlem6  25844  iblcnlem  25913  dvfsumlem4  26153  aannenlem1  26454  aannenlem2  26455  ulmval  26505  nodense  27818  nosupprefixmo  27826  noinfprefixmo  27827  nosupcbv  27828  nosupfv  27832  noinfcbv  27843  noinffv  27847  noetalem2  27868  eqcuts  27940  no2indlesm  28109  no3inds  28113  addsproplem3  28126  negsproplem3  28185  mulsproplem10  28280  bdayfinbndcbv  28621  bdayfinbndlem1  28622  bdayfinbndlem2  28623  istrkgb  28686  istrkge  28688  istrkgld  28690  istrkg2ld  28691  istrkg3ld  28692  axtgupdim2  28702  axtgeucl  28703  trgcgrg  28746  ishlg  28833  colline  28881  iscgra  29073  isinag  29106  brbtwn  29186  axpaschlem  29227  axlowdim  29248  axeuclid  29250  eengtrkge  29274  issubgr  29558  nb3grpr  29669  nb3grpr2  29670  cplgr3v  29722  wksfval  29896  iswlk  29897  upgr2wlk  29953  wlkiswwlks2  30161  wwlksnextfun  30184  wwlksnextinj  30185  wwlksnextbij  30188  wwlksnextprop  30198  2wlkdlem4  30214  umgr2wlk  30235  usgrwwlks2on  30244  umgrwwlks2on  30245  elwspths2spth  30256  isclwwlk  30272  clwlkclwwlklem1  30287  erclwwlkeq  30306  clwwlkn1loopb  30331  erclwwlkneq  30355  s2elclwwlknon2  30392  3wlkdlem5  30451  3wlkdlem6  30453  3wlkdlem9  30456  3wlkdlem10  30457  uhgr3cyclex  30470  upgr4cycl4dv4e  30473  frgr3v  30563  3cyclfrgrrn1  30573  extwwlkfabel  30641  isplig  30765  lpni  30769  isgrpo  30786  vciOLD  30850  isvclem  30866  isnvlem  30899  sspval  31012  isssp  31013  ajfval  31098  dipdir  31131  siilem2  31141  issh  31497  elunop2  32302  superpos  32643  padct  33000  isslmd  33459  slmdlema  33460  subsdrg  33558  elrspunidl  33676  constrcbvlem  34086  locfinreflem  34171  locfinref  34172  zarcmplem  34212  zhmnrg  34296  ismntoplly  34356  issiga  34443  isrnsiga  34444  isldsys  34487  rossros  34511  ismeas  34530  isrnmeas  34531  pmeasmono  34655  pmeasadd  34656  istrkg2d  34994  axtgupdim2ALTV  34996  afsval  35002  brafs  35003  bnj919  35097  bnj976  35107  bnj607  35245  bnj873  35253  fineqvnttrclse  35456  tz9.1regs  35466  cvmlift3lem2  35707  cvmlift3lem6  35711  cvmlift3lem7  35712  cvmlift3lem9  35714  cvmlift3  35715  mclsppslem  35970  dfon2lem1  36168  dfon2lem3  36170  dfon2lem7  36174  brofs  36392  ofscom  36394  btwnouttr  36411  brifs  36430  cgr3com  36440  brcolinear  36446  brfs  36466  prodeq12sdv  36615  cbvproddavw2  36693  unblimceq0lem  36980  knoppndvlem21  37006  rdgeqoa  37899  poimirlem4  38158  poimirlem27  38181  mblfinlem3  38193  indexa  38267  sdclem1  38277  fdc  38279  neificl  38287  heiborlem2  38346  isass  38380  ismndo2  38408  isrngo  38431  rngomndo  38469  isgrpda  38489  igenval2  38600  eleqvrels2  39210  eleqvrels3  39211  eqvreleq  39220  lshpset2N  39778  isopos  39839  oposlem  39841  cmtfvalN  39869  cvrfval  39927  3dimlem1  40117  3dim1lem5  40125  lplni2  40196  lvoli2  40240  4atlem11  40268  dalawlem15  40544  cdlemftr3  41224  tendofset  41417  tendoset  41418  istendo  41419  cdlemk28-3  41567  cdlemkid3N  41592  cdlemkid4  41593  lpolsetN  42141  islpolN  42142  lpolconN  42146  isprimroot  42745  aks6d1c1p1  42759  ismrc  43319  rabren3dioph  43429  irrapxlem5  43440  rmydioph  43628  mpaaeu  43764  mpaaval  43765  mpaalem  43766  naddwordnexlem4  44015  dfsucon  44136  minregex  44147  dfrtrcl3  44346  brco3f1o  44646  grumnud  44883  modelaxreplem1  45574  modelaxreplem2  45575  modelaxrep  45577  eliooshift  46109  stoweidlem5  46606  stoweidlem18  46619  stoweidlem28  46629  stoweidlem31  46632  stoweidlem41  46642  stoweidlem43  46644  stoweidlem44  46645  stoweidlem45  46646  stoweidlem51  46652  stoweidlem55  46656  stoweidlem59  46660  issal  46915  fundcmpsurbijinjpreimafv  48040  fundcmpsurbijinj  48043  fundcmpsurinjALT  48045  ichnreuop  48105  proththdlem  48249  6gbe  48420  8gbe  48422  bgoldbtbndlem2  48455  bgoldbtbndlem3  48456  bgoldbtbnd  48458  grtriproplem  48588  grtri  48589  grtrif1o  48591  isgrtri  48592  grimgrtri  48598  usgrexmpl1tri  48674  gpgvtx0  48702  gpgvtx1  48703  gpgedgvtx0  48710  gpgedgvtx1  48711  upwlksfval  48784  isupwlk  48785  el0ldep  49126  ldepspr  49133  lmod1  49152  zlmodzxzldep  49164  catprs  49669  catprsc  49671  prsthinc  50122  2arwcatlem1  50253  cnelsubclem  50261