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  2138  limeq  6313  f13dfv  7203  epne3  7701  oteqimp  7935  xpord2lem  8067  poxp2  8068  xpord3lem  8074  xpord3pred  8077  csbfrecsg  8209  frrlem1  8211  frrlem13  8223  smoeq  8265  on2ind  8579  on3ind  8580  naddasslem1  8604  naddasslem2  8605  naddass  8606  ereq1  8624  sbthfi  9103  indexfi  9239  hartogslem1  9423  brttrcl2  9599  ssttrcl  9600  ttrcltr  9601  ttrclss  9605  ttrclselem2  9611  tz9.1  9614  updjud  9822  alephval3  9996  cofsmo  10155  cfsmolem  10156  alephsing  10162  axdc3lem2  10337  axdc3lem3  10338  axdc3  10340  axdc4lem  10341  zornn0g  10391  fpwwe2lem4  10520  canthwelem  10536  canthwe  10537  pwfseqlem4a  10547  pwfseqlem4  10548  elwina  10572  elina  10573  iswun  10590  elgrug  10678  iccshftr  13381  iccshftl  13383  iccdil  13385  icccntr  13387  fzaddel  13453  elfzomelpfzo  13667  axdc4uzlem  13885  hash3tpb  14397  wrdl1s1  14517  wwlktovf  14858  wwlktovf1  14859  wwlktovfo  14860  wrd2f1tovbij  14862  dfrtrcl2  14964  sqrmo  15153  resqrtcl  15155  resqrtthlem  15156  sqrtneg  15169  sqreu  15263  sqrtthlem  15265  eqsqrtd  15270  prodeq1f  15808  prodeq1  15809  zprod  15839  divalglem10  16308  dfgcd2  16452  coprmprod  16567  pythagtriplem18  16739  pythagtriplem19  16740  prmgaplem3  16960  prmgaplem4  16961  isstruct2  17055  imasval  17410  mreexexlemd  17545  catidd  17581  iscatd2  17582  subsubc  17755  isfunc  17766  funcres2b  17799  ispos  18215  posi  18218  isposd  18223  pospropd  18226  resspos  18330  isps  18469  imasmnd2  18677  sgrp2rid2ex  18830  imasgrp2  18963  psgnunilem3  19403  isrngd  20086  imasrng  20090  isringd  20204  imasring  20243  subrngpropd  20478  isdrngd  20675  isdrngdOLD  20677  islmod  20792  lmodlema  20793  islmodd  20794  lmodprop2d  20852  lmhmpropd  21002  isphl  21560  isphld  21586  phlpropd  21587  mdetunilem3  22524  mdetunilem9  22530  fiinopn  22811  iscldtop  23005  lmfval  23142  connsuba  23330  1stcfb  23355  2ndcctbss  23365  subislly  23391  ptval  23480  elpt  23482  elptr  23483  upxp  23533  isfbas  23739  ustval  24113  isust  24114  ustincl  24118  ustdiag  24119  ustinvel  24120  ustexhalf  24121  ust0  24130  imasdsf1olem  24283  tngngp3  24566  lmhmclm  25009  iscph  25092  iscau2  25199  pmltpclem1  25371  isi1f  25597  mbfi1fseqlem6  25643  iblcnlem  25712  dvfsumlem4  25958  aannenlem1  26258  aannenlem2  26259  ulmval  26311  nodense  27626  nosupprefixmo  27634  noinfprefixmo  27635  nosupcbv  27636  nosupfv  27640  noinfcbv  27651  noinffv  27655  noetalem2  27676  eqscut  27741  no2indslem  27892  no3inds  27896  addsproplem3  27909  negsproplem3  27967  mulsproplem10  28059  istrkgb  28428  istrkge  28430  istrkgld  28432  istrkg2ld  28433  istrkg3ld  28434  axtgupdim2  28444  axtgeucl  28445  trgcgrg  28488  ishlg  28575  colline  28622  iscgra  28782  isinag  28811  brbtwn  28872  axpaschlem  28913  axlowdim  28934  axeuclid  28936  eengtrkge  28960  issubgr  29244  nb3grpr  29355  nb3grpr2  29356  cplgr3v  29408  wksfval  29583  iswlk  29584  upgr2wlk  29640  wlkiswwlks2  29848  wwlksnextfun  29871  wwlksnextinj  29872  wwlksnextbij  29875  wwlksnextprop  29885  2wlkdlem4  29901  umgr2wlk  29922  umgrwwlks2on  29930  elwspths2spth  29940  isclwwlk  29956  clwlkclwwlklem1  29971  erclwwlkeq  29990  clwwlkn1loopb  30015  erclwwlkneq  30039  s2elclwwlknon2  30076  3wlkdlem5  30135  3wlkdlem6  30137  3wlkdlem9  30140  3wlkdlem10  30141  uhgr3cyclex  30154  upgr4cycl4dv4e  30157  frgr3v  30247  3cyclfrgrrn1  30257  extwwlkfabel  30325  isplig  30448  lpni  30452  isgrpo  30469  vciOLD  30533  isvclem  30549  isnvlem  30582  sspval  30695  isssp  30696  ajfval  30781  dipdir  30814  siilem2  30824  issh  31180  elunop2  31985  superpos  32326  padct  32693  isslmd  33163  slmdlema  33164  subsdrg  33256  elrspunidl  33385  constrcbvlem  33760  locfinreflem  33845  locfinref  33846  zarcmplem  33886  zhmnrg  33970  ismntoplly  34030  issiga  34117  isrnsiga  34118  isldsys  34161  rossros  34185  ismeas  34204  isrnmeas  34205  pmeasmono  34329  pmeasadd  34330  istrkg2d  34671  axtgupdim2ALTV  34673  afsval  34676  brafs  34677  bnj919  34771  bnj976  34781  bnj607  34920  bnj873  34928  tz9.1regs  35122  fineqvnttrclse  35136  cvmlift3lem2  35356  cvmlift3lem6  35360  cvmlift3lem7  35361  cvmlift3lem9  35363  cvmlift3  35364  mclsppslem  35619  dfon2lem1  35817  dfon2lem3  35819  dfon2lem7  35823  brofs  36039  ofscom  36041  btwnouttr  36058  brifs  36077  cgr3com  36087  brcolinear  36093  brfs  36113  prodeq12sdv  36252  cbvproddavw2  36330  unblimceq0lem  36540  knoppndvlem21  36566  rdgeqoa  37404  poimirlem4  37664  poimirlem27  37687  mblfinlem3  37699  indexa  37773  sdclem1  37783  fdc  37785  neificl  37793  heiborlem2  37852  isass  37886  ismndo2  37914  isrngo  37937  rngomndo  37975  isgrpda  37995  igenval2  38106  eleqvrels2  38629  eleqvrels3  38630  eqvreleq  38639  lshpset2N  39158  isopos  39219  oposlem  39221  cmtfvalN  39249  cvrfval  39307  3dimlem1  39497  3dim1lem5  39505  lplni2  39576  lvoli2  39620  4atlem11  39648  dalawlem15  39924  cdlemftr3  40604  tendofset  40797  tendoset  40798  istendo  40799  cdlemk28-3  40947  cdlemkid3N  40972  cdlemkid4  40973  lpolsetN  41521  islpolN  41522  lpolconN  41526  isprimroot  42126  aks6d1c1p1  42140  ismrc  42734  rabren3dioph  42848  irrapxlem5  42859  rmydioph  43047  mpaaeu  43183  mpaaval  43184  mpaalem  43185  naddwordnexlem4  43434  dfsucon  43556  minregex  43567  dfrtrcl3  43766  brco3f1o  44066  grumnud  44319  modelaxreplem1  45011  modelaxreplem2  45012  modelaxrep  45014  eliooshift  45546  stoweidlem5  46043  stoweidlem18  46056  stoweidlem28  46066  stoweidlem31  46069  stoweidlem41  46079  stoweidlem43  46081  stoweidlem44  46082  stoweidlem45  46083  stoweidlem51  46089  stoweidlem55  46093  stoweidlem59  46097  issal  46352  fundcmpsurbijinjpreimafv  47438  fundcmpsurbijinj  47441  fundcmpsurinjALT  47443  ichnreuop  47503  proththdlem  47644  6gbe  47802  8gbe  47804  bgoldbtbndlem2  47837  bgoldbtbndlem3  47838  bgoldbtbnd  47840  grtriproplem  47970  grtri  47971  grtrif1o  47973  isgrtri  47974  grimgrtri  47980  usgrexmpl1tri  48056  gpgvtx0  48084  gpgvtx1  48085  gpgedgvtx0  48092  gpgedgvtx1  48093  upwlksfval  48166  isupwlk  48167  el0ldep  48498  ldepspr  48505  lmod1  48524  zlmodzxzldep  48536  catprs  49043  catprsc  49045  prsthinc  49496  2arwcatlem1  49627  cnelsubclem  49635