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

Theorem simpr3 1245
Description: Simplification of conjunction. (Contributed by Jeff Hankins, 17-Nov-2009.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)
Assertion
Ref Expression
simpr3 ((𝜑 ∧ (𝜓𝜒𝜃)) → 𝜃)

Proof of Theorem simpr3
StepHypRef Expression
1 simpr 473 . 2 ((𝜑𝜃) → 𝜃)
213ad2antr3 1234 1 ((𝜑 ∧ (𝜓𝜒𝜃)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  simplr3OLD  1273  simprr3OLD  1285  simpr13  1344  simpr23  1350  simpr33  1356  simp1r3  1363  simp2r3  1369  simp3r3  1375  3anandis  1588  funopsn  6635  fpr2g  6698  isopolem  6817  fr3nr  7207  suppfnss  7552  suppfnssOLD  7553  elfir  8558  intrnfi  8559  fisupcl  8612  cnfcomlem  8841  ackbij1lem15  9339  pwfseqlem4a  9766  pwfseqlem4  9767  eluzuzle  11911  xlesubadd  12309  elioc2  12452  elico2  12453  elicc2  12454  fseq1p1m1  12635  ccatswrd  13678  tanadd  15115  dvds2ln  15235  prmgaplem5  15974  prmgaplem8  15977  cshwsidrepsw  16010  ressress  16148  f1ovscpbl  16389  mreexexlem4d  16510  mreexexd  16511  2oppccomf  16587  fthmon  16789  fuccocl  16826  fucidcl  16827  invfuc  16836  initoeu2lem1  16866  curf2cl  17074  yonedalem4c  17120  yonedalem3  17123  pospo  17176  latjle12  17265  latjlej1  17268  latnlej2  17274  latlem12  17281  latmlem1  17284  latledi  17292  latjass  17298  latj12  17299  latj32  17300  latj13  17301  latj31  17302  latjrot  17303  latjjdi  17306  latjjdir  17307  latdisdlem  17392  prdsmndd  17526  imasmnd2  17530  imasmnd  17531  frmdmnd  17599  grpsubadd  17706  grpaddsubass  17708  grpsubsub4  17711  grppnpcan2  17712  grpnpncan  17713  grpnnncan2  17715  imasgrp2  17733  imasgrp  17734  mulgnndir  17771  mulgnn0dir  17772  mulgnnass  17777  mulgnn0ass  17778  mulgass  17779  pwsmulg  17787  issubg2  17809  qusgrp  17849  galcan  17936  gacan  17937  oppgmnd  17983  symggrp  18019  pmtrprfv  18072  pmtr3ncom  18094  psgnunilem3  18115  frgp0  18372  cmn32  18410  cmn12  18412  abladdsub  18419  ablsubsub23  18429  mulgdi  18431  mulgsubdi  18434  dprdss  18628  dprdf1o  18631  dprdsn  18635  dmdprdsplit  18646  pgpfac1lem5  18678  srgi  18711  ringi  18760  prdsringd  18812  imasring  18819  opprring  18831  mulgass3  18837  dvrass  18890  kerf1hrm  18945  subrgunit  19000  issubrg2  19002  abvdiv  19039  lss1  19141  lsssn0  19150  islss3  19164  prdslmodd  19174  islmhm2  19243  lspsolv  19349  lbsextlem4  19368  sralmod  19394  issubassa  19531  sraassa  19532  psrbaglesupp  19575  psrbagcon  19578  psrgrp  19605  psrlmod  19608  psrring  19618  psrassa  19621  mpllsslem  19642  ipdi  20193  ipsubdir  20195  ipsubdi  20196  ipassr  20199  ipassr2  20200  isphld  20207  ocvlss  20224  mamudm  20402  matring  20457  matassa  20458  ofco2  20466  scmatlss  20540  ma1repveval  20586  mdetunilem1  20627  mdetunilem9  20635  monmatcollpw  20795  iinopn  20918  restopnb  21191  subbascn  21270  nrmsep2  21372  isnrm3  21375  t1sep  21386  regsep2  21392  dnsconst  21394  dfconn2  21434  dislly  21512  tx1stc  21665  qtophmeo  21832  filss  21868  infil  21878  fsubbas  21882  filssufilg  21926  hauspwpwf1  22002  cnextcn  22082  tmdcn2  22104  psmettri  22327  isxmet2d  22343  xmettri  22367  xmetres2  22377  bldisj  22414  blss2ps  22419  blss2  22420  xmstri2  22482  mstri2  22483  xmstri  22484  mstri  22485  xmstri3  22486  mstri3  22487  msrtri  22488  comet  22529  met2ndci  22538  ngprcan  22625  ngplcan  22626  ngpsubcan  22629  nmtri2  22642  nrgdsdi  22680  nrgdsdir  22681  nlmdsdi  22696  nlmdsdir  22697  blcvx  22812  iocopnst  22950  icccvx  22960  pi1grplem  23059  pi1xfrf  23063  pi1cof  23069  clmpm1dir  23113  cmodscmulexp  23132  cvsdiv  23142  cvsdivcl  23143  cphdivcl  23192  cphsubdir  23218  cphsubdi  23219  bcthlem5  23335  rrxcph  23390  volfiniun  23526  volcn  23585  itg1val2  23663  dvconst  23892  dvlip  23968  ftc1a  24012  ulmdvlem3  24368  ang180  24756  cvxcl  24923  scvxcvx  24924  sgmmul  25138  logexprlim  25162  dchrabl  25191  motgrp  25650  iscgra1  25914  cgrane2  25917  cgrane4  25919  cgrahl1  25920  cgrahl2  25921  cgracgr  25922  cgratr  25927  cgrabtwn  25929  cgrahl  25930  dfcgra2  25933  sacgr  25934  f1otrge  25964  xmstrkgc  25978  colinearalglem1  25998  colinearalg  26002  axcgrtr  26007  axlowdimlem16  26049  axeuclidlem  26054  axcontlem4  26059  axcontlem7  26062  axcontlem12  26067  eengtrkg  26077  eengtrkge  26078  edglnl  26251  subgruhgredgd  26390  nbfusgrlevtxm2  26494  upgrwlkdvde  26859  crctcshwlkn0lem5  26933  crctcshwlkn0  26940  umgrwwlks2on  27096  rusgrnumwwlks  27114  clwlkclwwlkfo  27150  3spthd  27347  frgr2wwlkeqm  27504  dlwwlknondlwlknonf1o  27543  numclwwlk5  27574  friendship  27585  grpomuldivass  27722  ablodivdiv4  27735  dipdi  28024  dipsubdi  28030  disjdsct  29805  omndmul2  30035  archiabllem2c  30072  dvrdir  30113  dvrcan5  30116  reofld  30163  pstmfval  30262  qqhval2lem  30348  qqhvq  30354  esumcvg  30471  sigaclcu  30503  measdivcstOLD  30610  measdivcst  30611  carsggect  30703  tgoldbachgtd  31063  bnj970  31338  bnj910  31339  erdszelem9  31502  cvmseu  31579  elmrsubrn  31738  frrlem11  32111  noprefixmo  32167  nosupbnd1  32179  ssltsep  32224  cgrid2  32429  btwncomim  32439  btwnswapid  32443  trisegint  32454  cgrxfr  32481  btwnxfr  32482  brofs2  32503  brifs2  32504  endofsegid  32511  btwnconn1lem11  32523  btwnconn2  32528  segcon2  32531  seglemin  32539  segletr  32540  btwnsegle  32543  colinbtwnle  32544  broutsideof2  32548  btwnoutside  32551  broutsideof3  32552  outsideoftr  32555  outsidele  32558  ellines  32578  linethrueu  32582  unbdqndv2  32817  poimirlem28  33748  ftc1anc  33803  sdclem1  33848  sstotbnd2  33882  ismndo1  33981  zerdivemp1x  34055  isdrngo2  34066  iscringd  34106  lsmsat  34786  lfladdcl  34849  lflnegcl  34853  lflvscl  34855  lshpkrlem4  34891  lshpkrlem6  34893  ldualgrplem  34923  lduallmodlem  34930  latmassOLD  35007  latm12  35008  latm32  35009  latmrot  35010  latmmdiN  35012  latmmdir  35013  omlfh1N  35036  omlfh3N  35037  cvrnbtwn2  35053  cvlexchb1  35108  cvlexch3  35110  cvlexch4N  35111  cvlatexchb1  35112  cvlsupr2  35121  hlatjass  35148  hlatj12  35149  hlatj32  35150  cvrat  35200  atcvrj0  35206  cvrat2  35207  atltcvr  35213  atexchltN  35219  cvrat3  35220  cvrat4  35221  atbtwnexOLDN  35225  atbtwnex  35226  3dimlem3  35239  3dimlem3OLDN  35240  3at  35268  2atneat  35293  llncmp  35300  2at0mat0  35303  2atmat0  35304  islpln2a  35326  llncvrlpln  35336  lplncmp  35340  3atnelvolN  35364  4atlem11  35387  lplncvrlvol  35394  lvolcmp  35395  2atm2atN  35563  elpaddatriN  35581  elpadd2at2  35585  paddasslem8  35605  paddasslem17  35614  paddass  35616  padd12N  35617  paddssw1  35621  pmodlem2  35625  pmodN  35628  pmapjlln1  35633  atmod1i2  35637  pexmidlem2N  35749  pexmidlem7N  35754  pl42lem2N  35758  pl42lem3N  35759  pl42lem4N  35760  pl42N  35761  lhp2lt  35779  lhpm0atN  35807  lautlt  35869  lautcvr  35870  lautj  35871  lautm  35872  ltrneq2  35926  cdleme1b  36005  cdleme3b  36008  cdleme3c  36009  cdleme9b  36031  cdlemefs27cl  36192  cdleme42mN  36266  cdlemg4c  36391  trljco  36519  tgrpgrplem  36528  tendoplass  36562  tendodi1  36563  tendodi2  36564  erngplus2  36583  erngplus2-rN  36591  cdlemk36  36692  erngdvlem3  36769  erngdvlem3-rN  36777  dvaplusgv  36789  tendospass  36798  tendospdi1  36799  dvalveclem  36804  dialss  36825  dvhvaddass  36876  dvhopvsca  36881  dvhlveclem  36887  diblss  36949  diclss  36972  diclspsn  36973  cdlemn11pre  36989  dihmeetlem12N  37097  dihmeetlem16N  37101  dihmeetlem17N  37102  dvh4dimN  37226  lpolsatN  37267  lpolpolsatN  37268  dochpolN  37269  lclkr  37312  lclkrs  37318  lcfr  37364  irrapxlem6  37891  jm2.26lem3  38067  mpaamn  38225  mendring  38261  mendlmod  38262  mendassa  38263  neicvgel1  38915  rfcnpre4  39685  fmuldfeq  40293  stoweidlem43  40737  stoweidlem52  40746  stoweidlem53  40747  stoweidlem56  40750  issmfgt  41445  issmfge  41458  iccelpart  41942  pfxccat3a  42002  fmtnoprmfac1  42050  fmtnoprmfac2  42052  copissgrp  42374  ringrng  42445  cznrng  42521  funcringcsetcALTV2lem9  42610  funcringcsetclem9ALTV  42633  linccl  42769  lincsumscmcl  42788  ldepsprlem  42827  lincresunit3lem1  42834
  Copyright terms: Public domain W3C validator