Theorem 3anbi123d 1436

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

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

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 1089

This theorem is referenced by:  3anbi12d  1437  3anbi13d  1438  3anbi23d  1439  ax12wdemo  2135  limeq  6407  f13dfv  7310  epne3  7808  oteqimp  8049  xpord2lem  8183  poxp2  8184  xpord3lem  8190  xpord3pred  8193  csbfrecsg  8325  frrlem1  8327  frrlem13  8339  wfrlem1OLD  8364  wfrlem15OLD  8379  smoeq  8406  on2ind  8725  on3ind  8726  naddasslem1  8750  naddasslem2  8751  naddass  8752  ereq1  8770  sbthfi  9265  indexfi  9430  hartogslem1  9611  brttrcl2  9783  ssttrcl  9784  ttrcltr  9785  ttrclss  9789  ttrclselem2  9795  tz9.1  9798  updjud  10003  alephval3  10179  cofsmo  10338  cfsmolem  10339  alephsing  10345  axdc3lem2  10520  axdc3lem3  10521  axdc3  10523  axdc4lem  10524  zornn0g  10574  fpwwe2lem4  10703  canthwelem  10719  canthwe  10720  pwfseqlem4a  10730  pwfseqlem4  10731  elwina  10755  elina  10756  iswun  10773  elgrug  10861  iccshftr  13546  iccshftl  13548  iccdil  13550  icccntr  13552  fzaddel  13618  elfzomelpfzo  13821  axdc4uzlem  14034  hash3tpb  14544  wrdl1s1  14662  wwlktovf  15005  wwlktovf1  15006  wwlktovfo  15007  wrd2f1tovbij  15009  dfrtrcl2  15111  sqrmo  15300  resqrtcl  15302  resqrtthlem  15303  sqrtneg  15316  sqreu  15409  sqrtthlem  15411  eqsqrtd  15416  prodeq1f  15954  prodeq1  15955  zprod  15985  divalglem10  16450  dfgcd2  16593  coprmprod  16708  pythagtriplem18  16879  pythagtriplem19  16880  prmgaplem3  17100  prmgaplem4  17101  isstruct2  17196  imasval  17571  mreexexlemd  17702  catidd  17738  iscatd2  17739  subsubc  17917  isfunc  17928  funcres2b  17961  ispos  18384  posi  18387  isposd  18393  pospropd  18397  isps  18638  imasmnd2  18809  sgrp2rid2ex  18962  imasgrp2  19095  psgnunilem3  19538  isrngd  20200  imasrng  20204  isringd  20314  imasring  20353  subrngpropd  20594  isdrngd  20787  isdrngdOLD  20789  islmod  20884  lmodlema  20885  islmodd  20886  lmodprop2d  20944  lmhmpropd  21095  isphl  21669  isphld  21695  phlpropd  21696  mdetunilem3  22641  mdetunilem9  22647  fiinopn  22928  iscldtop  23124  lmfval  23261  connsuba  23449  1stcfb  23474  2ndcctbss  23484  subislly  23510  ptval  23599  elpt  23601  elptr  23602  upxp  23652  isfbas  23858  ustval  24232  isust  24233  ustincl  24237  ustdiag  24238  ustinvel  24239  ustexhalf  24240  ust0  24249  imasdsf1olem  24404  tngngp3  24698  lmhmclm  25139  iscph  25223  iscau2  25330  pmltpclem1  25502  isi1f  25728  mbfi1fseqlem6  25775  iblcnlem  25844  dvfsumlem4  26090  aannenlem1  26388  aannenlem2  26389  ulmval  26441  nodense  27755  nosupprefixmo  27763  noinfprefixmo  27764  nosupcbv  27765  nosupfv  27769  noinfcbv  27780  noinffv  27784  noetalem2  27805  eqscut  27868  no2indslem  28005  no3inds  28009  addsproplem3  28022  negsproplem3  28080  mulsproplem10  28169  istrkgb  28481  istrkge  28483  istrkgld  28485  istrkg2ld  28486  istrkg3ld  28487  axtgupdim2  28497  axtgeucl  28498  trgcgrg  28541  ishlg  28628  colline  28675  iscgra  28835  isinag  28864  brbtwn  28932  axpaschlem  28973  axlowdim  28994  axeuclid  28996  eengtrkge  29020  issubgr  29306  nb3grpr  29417  nb3grpr2  29418  cplgr3v  29470  wksfval  29645  iswlk  29646  upgr2wlk  29704  wlkiswwlks2  29908  wwlksnextfun  29931  wwlksnextinj  29932  wwlksnextbij  29935  wwlksnextprop  29945  2wlkdlem4  29961  umgr2wlk  29982  umgrwwlks2on  29990  elwspths2spth  30000  isclwwlk  30016  clwlkclwwlklem1  30031  erclwwlkeq  30050  clwwlkn1loopb  30075  erclwwlkneq  30099  s2elclwwlknon2  30136  3wlkdlem5  30195  3wlkdlem6  30197  3wlkdlem9  30200  3wlkdlem10  30201  uhgr3cyclex  30214  upgr4cycl4dv4e  30217  frgr3v  30307  3cyclfrgrrn1  30317  extwwlkfabel  30385  isplig  30508  lpni  30512  isgrpo  30529  vciOLD  30593  isvclem  30609  isnvlem  30642  sspval  30755  isssp  30756  ajfval  30841  dipdir  30874  siilem2  30884  issh  31240  elunop2  32045  superpos  32386  padct  32733  resspos  32939  isslmd  33181  slmdlema  33182  elrspunidl  33421  locfinreflem  33786  locfinref  33787  zarcmplem  33827  zhmnrg  33913  ismntoplly  33971  issiga  34076  isrnsiga  34077  isldsys  34120  rossros  34144  ismeas  34163  isrnmeas  34164  pmeasmono  34289  pmeasadd  34290  istrkg2d  34643  axtgupdim2ALTV  34645  afsval  34648  brafs  34649  bnj919  34743  bnj976  34753  bnj607  34892  bnj873  34900  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  36184  cbvproddavw2  36262  unblimceq0lem  36472  knoppndvlem21  36498  rdgeqoa  37336  poimirlem4  37584  poimirlem27  37607  mblfinlem3  37619  indexa  37693  sdclem1  37703  fdc  37705  neificl  37713  heiborlem2  37772  isass  37806  ismndo2  37834  isrngo  37857  rngomndo  37895  isgrpda  37915  igenval2  38026  eleqvrels2  38548  eleqvrels3  38549  eqvreleq  38558  lshpset2N  39075  isopos  39136  oposlem  39138  cmtfvalN  39166  cvrfval  39224  3dimlem1  39415  3dim1lem5  39423  lplni2  39494  lvoli2  39538  4atlem11  39566  dalawlem15  39842  cdlemftr3  40522  tendofset  40715  tendoset  40716  istendo  40717  cdlemk28-3  40865  cdlemkid3N  40890  cdlemkid4  40891  lpolsetN  41439  islpolN  41440  lpolconN  41444  isprimroot  42050  aks6d1c1p1  42064  ismrc  42657  rabren3dioph  42771  irrapxlem5  42782  rmydioph  42971  mpaaeu  43107  mpaaval  43108  mpaalem  43109  naddwordnexlem4  43363  dfsucon  43485  minregex  43496  dfrtrcl3  43695  brco3f1o  43995  grumnud  44255  eliooshift  45424  stoweidlem5  45926  stoweidlem18  45939  stoweidlem28  45949  stoweidlem31  45952  stoweidlem41  45962  stoweidlem43  45964  stoweidlem44  45965  stoweidlem45  45966  stoweidlem51  45972  stoweidlem55  45976  stoweidlem59  45980  issal  46235  fundcmpsurbijinjpreimafv  47281  fundcmpsurbijinj  47284  fundcmpsurinjALT  47286  ichnreuop  47346  proththdlem  47487  6gbe  47645  8gbe  47647  bgoldbtbndlem2  47680  bgoldbtbndlem3  47681  bgoldbtbnd  47683  grtriproplem  47790  grtri  47791  grtrif1o  47793  isgrtri  47794  grimgrtri  47798  usgrexmpl1tri  47840  upwlksfval  47858  isupwlk  47859  el0ldep  48195  ldepspr  48202  lmod1  48221  zlmodzxzldep  48233  catprs  48678  catprsc  48680  prsthinc  48721