MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3anbi123d Structured version   Visualization version   GIF version

Theorem 3anbi123d 1429
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
StepHypRef Expression
1 bi3d.1 . . . 4 (𝜑 → (𝜓𝜒))
2 bi3d.2 . . . 4 (𝜑 → (𝜃𝜏))
31, 2anbi12d 630 . . 3 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜏)))
4 bi3d.3 . . 3 (𝜑 → (𝜂𝜁))
53, 4anbi12d 630 . 2 (𝜑 → (((𝜓𝜃) ∧ 𝜂) ↔ ((𝜒𝜏) ∧ 𝜁)))
6 df-3an 1083 . 2 ((𝜓𝜃𝜂) ↔ ((𝜓𝜃) ∧ 𝜂))
7 df-3an 1083 . 2 ((𝜒𝜏𝜁) ↔ ((𝜒𝜏) ∧ 𝜁))
85, 6, 73bitr4g 315 1 (𝜑 → ((𝜓𝜃𝜂) ↔ (𝜒𝜏𝜁)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  w3a 1081
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 208  df-an 397  df-3an 1083
This theorem is referenced by:  3anbi12d  1430  3anbi13d  1431  3anbi23d  1432  ax12wdemo  2132  limeq  6201  f13dfv  7025  epne3  7483  oteqimp  7699  wfrlem1  7945  wfrlem15  7960  smoeq  7978  ereq1  8286  indexfi  8821  hartogslem1  8995  tz9.1  9160  updjud  9352  alephval3  9525  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  12862  iccshftl  12864  iccdil  12866  icccntr  12868  fzaddel  12931  elfzomelpfzo  13131  axdc4uzlem  13341  wrdl1s1  13958  wwlktovf  14310  wwlktovf1  14311  wwlktovfo  14312  wrd2f1tovbij  14314  dfrtrcl2  14411  sqrmo  14601  resqrtcl  14603  resqrtthlem  14604  sqrtneg  14617  sqreu  14710  sqrtthlem  14712  eqsqrtd  14717  prodeq1f  15252  zprod  15281  divalglem10  15743  dfgcd2  15884  coprmprod  15995  pythagtriplem18  16159  pythagtriplem19  16160  prmgaplem3  16379  prmgaplem4  16380  isstruct2  16483  imasval  16774  mreexexlemd  16905  catidd  16941  iscatd2  16942  subsubc  17113  isfunc  17124  funcres2b  17157  ispos  17547  posi  17550  isposd  17555  pospropd  17734  isps  17802  imasmnd2  17936  sgrp2rid2ex  18025  imasgrp2  18144  psgnunilem3  18544  isringd  19255  imasring  19289  isdrngd  19447  islmod  19558  lmodlema  19559  islmodd  19560  lmodprop2d  19616  lmhmpropd  19765  assapropd  20020  isphl  20688  isphld  20714  phlpropd  20715  mdetunilem3  21139  mdetunilem9  21145  fiinopn  21425  iscldtop  21619  lmfval  21756  connsuba  21944  1stcfb  21969  2ndcctbss  21979  subislly  22005  ptval  22094  elpt  22096  elptr  22097  upxp  22147  isfbas  22353  ustval  22726  isust  22727  ustincl  22731  ustdiag  22732  ustinvel  22733  ustexhalf  22734  ust0  22743  imasdsf1olem  22898  tngngp3  23180  lmhmclm  23606  iscph  23689  iscau2  23795  pmltpclem1  23964  isi1f  24190  mbfi1fseqlem6  24236  iblcnlem  24304  dvfsumlem4  24541  aannenlem1  24832  aannenlem2  24833  ulmval  24883  istrkgb  26155  istrkge  26157  istrkgld  26159  istrkg2ld  26160  istrkg3ld  26161  axtgupdim2  26171  axtgeucl  26172  trgcgrg  26215  ishlg  26302  colline  26349  iscgra  26509  isinag  26538  brbtwn  26599  axpaschlem  26640  axlowdim  26661  axeuclid  26663  eengtrkge  26687  issubgr  26967  nb3grpr  27078  nb3grpr2  27079  cplgr3v  27131  wksfval  27305  iswlk  27306  upgr2wlk  27364  wlkiswwlks2  27567  wwlksnextfun  27590  wwlksnextinj  27591  wwlksnextbij  27594  wwlksnextprop  27605  2wlkdlem4  27621  umgr2wlk  27642  umgrwwlks2on  27650  elwspths2spth  27660  isclwwlk  27676  clwlkclwwlklem1  27691  erclwwlkeq  27710  clwwlkn1loopb  27735  erclwwlkneq  27760  s2elclwwlknon2  27797  3wlkdlem5  27856  3wlkdlem6  27858  3wlkdlem9  27861  3wlkdlem10  27862  uhgr3cyclex  27875  upgr4cycl4dv4e  27878  frgr3v  27968  3cyclfrgrrn1  27978  extwwlkfabel  28046  isplig  28167  lpni  28171  isgrpo  28188  vciOLD  28252  isvclem  28268  isnvlem  28301  sspval  28414  isssp  28415  ajfval  28500  dipdir  28533  siilem2  28543  issh  28899  elunop2  29704  superpos  30045  padct  30368  resspos  30560  isslmd  30744  slmdlema  30745  locfinreflem  30990  locfinref  30991  zhmnrg  31094  ismntoplly  31152  issiga  31257  isrnsiga  31258  isldsys  31301  rossros  31325  ismeas  31344  isrnmeas  31345  pmeasmono  31468  pmeasadd  31469  istrkg2d  31823  axtgupdim2ALTV  31825  afsval  31828  brafs  31829  bnj919  31924  bnj976  31935  bnj607  32074  bnj873  32082  cvmlift3lem2  32451  cvmlift3lem6  32455  cvmlift3lem7  32456  cvmlift3lem9  32458  cvmlift3  32459  mclsppslem  32714  dfon2lem1  32912  dfon2lem3  32914  dfon2lem7  32918  frrlem1  33007  frrlem13  33019  nodense  33080  noprefixmo  33086  nosupfv  33090  noetalem5  33105  noeta  33106  brofs  33350  ofscom  33352  btwnouttr  33369  brifs  33388  cgr3com  33398  brcolinear  33404  brfs  33424  unblimceq0lem  33729  knoppndvlem21  33755  csbwrecsg  34477  rdgeqoa  34520  poimirlem4  34763  poimirlem27  34786  mblfinlem3  34798  indexa  34876  sdclem1  34886  fdc  34888  neificl  34896  heiborlem2  34958  isass  34992  ismndo2  35020  isrngo  35043  rngomndo  35081  isgrpda  35101  igenval2  35212  eleqvrels2  35694  eleqvrels3  35695  eqvreleq  35704  lshpset2N  36122  isopos  36183  oposlem  36185  cmtfvalN  36213  cvrfval  36271  3dimlem1  36461  3dim1lem5  36469  lplni2  36540  lvoli2  36584  4atlem11  36612  dalawlem15  36888  cdlemftr3  37568  tendofset  37761  tendoset  37762  istendo  37763  cdlemk28-3  37911  cdlemkid3N  37936  cdlemkid4  37937  lpolsetN  38485  islpolN  38486  lpolconN  38490  ismrc  39163  rabren3dioph  39277  irrapxlem5  39288  rmydioph  39476  mpaaeu  39615  mpaaval  39616  mpaalem  39617  dfsucon  39754  dfrtrcl3  39943  brco3f1o  40248  grumnud  40487  eliooshift  41647  stoweidlem5  42156  stoweidlem18  42169  stoweidlem28  42179  stoweidlem31  42182  stoweidlem41  42192  stoweidlem43  42194  stoweidlem44  42195  stoweidlem45  42196  stoweidlem51  42202  stoweidlem55  42206  stoweidlem59  42210  issal  42465  ichnreuop  43466  proththdlem  43610  6gbe  43768  8gbe  43770  bgoldbtbndlem2  43803  bgoldbtbndlem3  43804  bgoldbtbnd  43806  upwlksfval  43842  isupwlk  43843  el0ldep  44353  ldepspr  44360  lmod1  44379  zlmodzxzldep  44391
  Copyright terms: Public domain W3C validator