Theorem 3anbi123d 1433

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084

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 400  df-3an 1086

This theorem is referenced by:  3anbi12d  1434  3anbi13d  1435  3anbi23d  1436  ax12wdemo  2136  limeq  6171  f13dfv  7009  epne3  7475  oteqimp  7690  wfrlem1  7937  wfrlem15  7952  smoeq  7970  ereq1  8279  indexfi  8816  hartogslem1  8990  tz9.1  9155  updjud  9347  alephval3  9521  cofsmo  9680  cfsmolem  9681  alephsing  9687  axdc3lem2  9862  axdc3lem3  9863  axdc3  9865  axdc4lem  9866  zornn0g  9916  fpwwe2lem5  10045  canthwelem  10061  canthwe  10062  pwfseqlem4a  10072  pwfseqlem4  10073  elwina  10097  elina  10098  iswun  10115  elgrug  10203  iccshftr  12864  iccshftl  12866  iccdil  12868  icccntr  12870  fzaddel  12936  elfzomelpfzo  13136  axdc4uzlem  13346  wrdl1s1  13959  wwlktovf  14311  wwlktovf1  14312  wwlktovfo  14313  wrd2f1tovbij  14315  dfrtrcl2  14413  sqrmo  14603  resqrtcl  14605  resqrtthlem  14606  sqrtneg  14619  sqreu  14712  sqrtthlem  14714  eqsqrtd  14719  prodeq1f  15254  zprod  15283  divalglem10  15743  dfgcd2  15884  coprmprod  15995  pythagtriplem18  16159  pythagtriplem19  16160  prmgaplem3  16379  prmgaplem4  16380  isstruct2  16485  imasval  16776  mreexexlemd  16907  catidd  16943  iscatd2  16944  subsubc  17115  isfunc  17126  funcres2b  17159  ispos  17549  posi  17552  isposd  17557  pospropd  17736  isps  17804  imasmnd2  17940  sgrp2rid2ex  18084  imasgrp2  18206  psgnunilem3  18616  isringd  19331  imasring  19365  isdrngd  19520  islmod  19631  lmodlema  19632  islmodd  19633  lmodprop2d  19689  lmhmpropd  19838  isphl  20317  isphld  20343  phlpropd  20344  assapropd  20558  mdetunilem3  21219  mdetunilem9  21225  fiinopn  21506  iscldtop  21700  lmfval  21837  connsuba  22025  1stcfb  22050  2ndcctbss  22060  subislly  22086  ptval  22175  elpt  22177  elptr  22178  upxp  22228  isfbas  22434  ustval  22808  isust  22809  ustincl  22813  ustdiag  22814  ustinvel  22815  ustexhalf  22816  ust0  22825  imasdsf1olem  22980  tngngp3  23262  lmhmclm  23692  iscph  23775  iscau2  23881  pmltpclem1  24052  isi1f  24278  mbfi1fseqlem6  24324  iblcnlem  24392  dvfsumlem4  24632  aannenlem1  24924  aannenlem2  24925  ulmval  24975  istrkgb  26249  istrkge  26251  istrkgld  26253  istrkg2ld  26254  istrkg3ld  26255  axtgupdim2  26265  axtgeucl  26266  trgcgrg  26309  ishlg  26396  colline  26443  iscgra  26603  isinag  26632  brbtwn  26693  axpaschlem  26734  axlowdim  26755  axeuclid  26757  eengtrkge  26781  issubgr  27061  nb3grpr  27172  nb3grpr2  27173  cplgr3v  27225  wksfval  27399  iswlk  27400  upgr2wlk  27458  wlkiswwlks2  27661  wwlksnextfun  27684  wwlksnextinj  27685  wwlksnextbij  27688  wwlksnextprop  27698  2wlkdlem4  27714  umgr2wlk  27735  umgrwwlks2on  27743  elwspths2spth  27753  isclwwlk  27769  clwlkclwwlklem1  27784  erclwwlkeq  27803  clwwlkn1loopb  27828  erclwwlkneq  27852  s2elclwwlknon2  27889  3wlkdlem5  27948  3wlkdlem6  27950  3wlkdlem9  27953  3wlkdlem10  27954  uhgr3cyclex  27967  upgr4cycl4dv4e  27970  frgr3v  28060  3cyclfrgrrn1  28070  extwwlkfabel  28138  isplig  28259  lpni  28263  isgrpo  28280  vciOLD  28344  isvclem  28360  isnvlem  28393  sspval  28506  isssp  28507  ajfval  28592  dipdir  28625  siilem2  28635  issh  28991  elunop2  29796  superpos  30137  padct  30481  resspos  30672  isslmd  30880  slmdlema  30881  elrspunidl  31014  locfinreflem  31193  locfinref  31194  zarcmplem  31234  zhmnrg  31318  ismntoplly  31376  issiga  31481  isrnsiga  31482  isldsys  31525  rossros  31549  ismeas  31568  isrnmeas  31569  pmeasmono  31692  pmeasadd  31693  istrkg2d  32047  axtgupdim2ALTV  32049  afsval  32052  brafs  32053  bnj919  32148  bnj976  32159  bnj607  32298  bnj873  32306  cvmlift3lem2  32680  cvmlift3lem6  32684  cvmlift3lem7  32685  cvmlift3lem9  32687  cvmlift3  32688  mclsppslem  32943  dfon2lem1  33141  dfon2lem3  33143  dfon2lem7  33147  frrlem1  33236  frrlem13  33248  nodense  33309  noprefixmo  33315  nosupfv  33319  noetalem5  33334  noeta  33335  brofs  33579  ofscom  33581  btwnouttr  33598  brifs  33617  cgr3com  33627  brcolinear  33633  brfs  33653  unblimceq0lem  33958  knoppndvlem21  33984  csbwrecsg  34744  rdgeqoa  34787  poimirlem4  35061  poimirlem27  35084  mblfinlem3  35096  indexa  35171  sdclem1  35181  fdc  35183  neificl  35191  heiborlem2  35250  isass  35284  ismndo2  35312  isrngo  35335  rngomndo  35373  isgrpda  35393  igenval2  35504  eleqvrels2  35987  eleqvrels3  35988  eqvreleq  35997  lshpset2N  36415  isopos  36476  oposlem  36478  cmtfvalN  36506  cvrfval  36564  3dimlem1  36754  3dim1lem5  36762  lplni2  36833  lvoli2  36877  4atlem11  36905  dalawlem15  37181  cdlemftr3  37861  tendofset  38054  tendoset  38055  istendo  38056  cdlemk28-3  38204  cdlemkid3N  38229  cdlemkid4  38230  lpolsetN  38778  islpolN  38779  lpolconN  38783  ismrc  39642  rabren3dioph  39756  irrapxlem5  39767  rmydioph  39955  mpaaeu  40094  mpaaval  40095  mpaalem  40096  dfsucon  40231  dfrtrcl3  40434  brco3f1o  40736  grumnud  40994  eliooshift  42143  stoweidlem5  42647  stoweidlem18  42660  stoweidlem28  42670  stoweidlem31  42673  stoweidlem41  42683  stoweidlem43  42685  stoweidlem44  42686  stoweidlem45  42687  stoweidlem51  42693  stoweidlem55  42697  stoweidlem59  42701  issal  42956  fundcmpsurbijinjpreimafv  43924  fundcmpsurbijinj  43927  fundcmpsurinjALT  43929  ichnreuop  43989  proththdlem  44131  6gbe  44289  8gbe  44291  bgoldbtbndlem2  44324  bgoldbtbndlem3  44325  bgoldbtbnd  44327  upwlksfval  44363  isupwlk  44364  el0ldep  44875  ldepspr  44882  lmod1  44901  zlmodzxzldep  44913