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

Theorem simpr3 1061
Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
Assertion
Ref Expression
simpr3 ((𝜑 ∧ (𝜓𝜒𝜃)) → 𝜃)

Proof of Theorem simpr3
StepHypRef Expression
1 simp3 1055 . 2 ((𝜓𝜒𝜃) → 𝜃)
21adantl 480 1 ((𝜑 ∧ (𝜓𝜒𝜃)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  simplr3  1097  simprr3  1103  simp1r3  1151  simp2r3  1157  simp3r3  1163  3anandis  1425  fpr2g  6357  isopolem  6472  fr3nr  6848  suppfnss  7184  elfir  8181  intrnfi  8182  fisupcl  8235  cnfcomlem  8456  ackbij1lem15  8916  pwfseqlem4a  9339  pwfseqlem4  9340  eluzuzle  11530  xlesubadd  11924  elioc2  12065  elico2  12066  elicc2  12067  fseq1p1m1  12240  ccatswrd  13256  modfsummods  14314  tanadd  14684  dvds2ln  14800  prmgaplem5  15545  prmgaplem8  15548  cshwsidrepsw  15586  ressress  15713  f1ovscpbl  15957  mreexexlem4d  16078  mreexexd  16079  mreexexdOLD  16080  2oppccomf  16156  fthmon  16358  fuccocl  16395  fucidcl  16396  invfuc  16405  initoeu2lem1  16435  curf2cl  16642  yonedalem4c  16688  yonedalem3  16691  pospo  16744  latjle12  16833  latjlej1  16836  latnlej2  16842  latlem12  16849  latmlem1  16852  latledi  16860  latjass  16866  latj12  16867  latj32  16868  latj13  16869  latj31  16870  latjrot  16871  latjjdi  16874  latjjdir  16875  latdisdlem  16960  prdsmndd  17094  imasmnd2  17098  imasmnd  17099  frmdmnd  17167  grpsubadd  17274  grpaddsubass  17276  grpsubsub4  17279  grppnpcan2  17280  grpnpncan  17281  grpnnncan2  17283  imasgrp2  17301  imasgrp  17302  mulgnndir  17340  mulgnndirOLD  17341  mulgnn0dir  17342  mulgnnass  17347  mulgnnassOLD  17348  mulgnn0ass  17349  mulgass  17350  pwsmulg  17358  issubg2  17380  qusgrp  17420  galcan  17508  gacan  17509  oppgmnd  17555  symggrp  17591  pmtrprfv  17644  pmtr3ncom  17666  psgnunilem3  17687  frgp0  17944  cmn32  17982  cmn12  17984  abladdsub  17991  ablsubsub23  18001  mulgdi  18003  mulgsubdi  18006  dprdss  18199  dprdf1o  18202  dprdsn  18206  dmdprdsplit  18217  pgpfac1lem5  18249  srgi  18282  ringi  18331  prdsringd  18383  imasring  18390  opprring  18402  mulgass3  18408  dvrass  18461  kerf1hrm  18514  subrgunit  18569  issubrg2  18571  abvdiv  18608  lss1  18708  lsssn0  18717  islss3  18728  prdslmodd  18738  islmhm2  18807  lspsolv  18912  lbsextlem4  18930  sralmod  18956  issubassa  19093  sraassa  19094  psrbaglesupp  19137  psrbagcon  19140  psrgrp  19167  psrlmod  19170  psrring  19180  psrassa  19183  mpllsslem  19204  ipdi  19751  ipsubdir  19753  ipsubdi  19754  ipassr  19757  ipassr2  19758  isphld  19765  ocvlss  19782  mamudm  19960  matring  20015  matassa  20016  ofco2  20023  scmatlss  20097  ma1repveval  20143  mdetunilem1  20184  mdetunilem9  20192  monmatcollpw  20350  iinopn  20479  restopnb  20736  subbascn  20815  nrmsep2  20917  isnrm3  20920  t1sep  20931  regsep2  20937  dnsconst  20939  dfcon2  20979  dislly  21057  tx1stc  21210  qtophmeo  21377  filss  21414  infil  21424  fsubbas  21428  filssufilg  21472  hauspwpwf1  21548  cnextcn  21628  tmdcn2  21650  psmettri  21873  isxmet2d  21889  xmettri  21913  xmetres2  21923  bldisj  21960  blss2ps  21965  blss2  21966  xmstri2  22028  mstri2  22029  xmstri  22030  mstri  22031  xmstri3  22032  mstri3  22033  msrtri  22034  comet  22075  met2ndci  22084  ngprcan  22171  ngplcan  22172  ngpsubcan  22175  nmtri2  22188  nrgdsdi  22226  nrgdsdir  22227  nlmdsdi  22242  nlmdsdir  22243  blcvx  22356  iocopnst  22494  icccvx  22504  pi1grplem  22604  pi1xfrf  22608  pi1cof  22614  clmpm1dir  22658  cmodscmulexp  22677  cvsdiv  22687  cvsdivcl  22688  cphdivcl  22734  cphsubdir  22760  cphsubdi  22761  bcthlem5  22877  rrxcph  22932  volfiniun  23066  volcn  23124  itg1val2  23201  dvconst  23430  dvlip  23504  ftc1a  23548  ulmdvlem3  23904  ang180  24288  cvxcl  24455  scvxcvx  24456  sgmmul  24670  logexprlim  24694  dchrabl  24723  motgrp  25183  iscgra1  25447  cgrane2  25450  cgrane4  25452  cgrahl1  25453  cgrahl2  25454  cgracgr  25455  cgratr  25460  cgrabtwn  25462  cgrahl  25463  dfcgra2  25466  sacgr  25467  f1otrge  25497  xmstrkgc  25511  colinearalglem1  25531  colinearalg  25535  axcgrtr  25540  axlowdimlem16  25582  axeuclidlem  25587  axcontlem4  25592  axcontlem7  25595  axcontlem12  25600  eengtrkg  25610  eengtrkge  25611  isspthonpth  25907  wlkdvspth  25931  usg2wotspth  26204  2pthwlkonot  26205  rusgranumwwlkg  26279  numclwwlk5  26432  friendship  26442  grpomuldivass  26572  ablodivdiv4  26585  ablonnncan  26587  dipdi  26875  dipsubdi  26881  disjdsct  28656  omndmul2  28836  archiabllem2c  28873  dvrdir  28914  dvrcan5  28917  reofld  28964  pstmfval  29060  qqhval2lem  29146  qqhvq  29152  esumcvg  29268  sigaclcu  29300  measdivcstOLD  29407  measdivcst  29408  carsggect  29500  bnj970  30064  bnj910  30065  erdszelem9  30228  cvmseu  30305  elmrsubrn  30464  cgrid2  31073  btwncomim  31083  btwnswapid  31087  trisegint  31098  cgrxfr  31125  btwnxfr  31126  brofs2  31147  brifs2  31148  endofsegid  31155  btwnconn1lem11  31167  btwnconn2  31172  segcon2  31175  seglemin  31183  segletr  31184  btwnsegle  31187  colinbtwnle  31188  broutsideof2  31192  btwnoutside  31195  broutsideof3  31196  outsideoftr  31199  outsidele  31202  ellines  31222  linethrueu  31226  unbdqndv2  31465  poimirlem28  32390  ftc1anc  32446  sdclem1  32492  sstotbnd2  32526  ismndo1  32625  zerdivemp1x  32699  isdrngo2  32710  iscringd  32750  lsmsat  33096  lfladdcl  33159  lflnegcl  33163  lflvscl  33165  lshpkrlem4  33201  lshpkrlem6  33203  ldualgrplem  33233  lduallmodlem  33240  latmassOLD  33317  latm12  33318  latm32  33319  latmrot  33320  latmmdiN  33322  latmmdir  33323  omlfh1N  33346  omlfh3N  33347  cvrnbtwn2  33363  cvlexchb1  33418  cvlexch3  33420  cvlexch4N  33421  cvlatexchb1  33422  cvlsupr2  33431  hlatjass  33457  hlatj12  33458  hlatj32  33459  cvrat  33509  atcvrj0  33515  cvrat2  33516  atltcvr  33522  atexchltN  33528  cvrat3  33529  cvrat4  33530  atbtwnexOLDN  33534  atbtwnex  33535  3dimlem3  33548  3dimlem3OLDN  33549  3at  33577  2atneat  33602  llncmp  33609  2at0mat0  33612  2atmat0  33613  islpln2a  33635  llncvrlpln  33645  lplncmp  33649  3atnelvolN  33673  4atlem11  33696  lplncvrlvol  33703  lvolcmp  33704  2atm2atN  33872  elpaddatriN  33890  elpadd2at2  33894  paddasslem8  33914  paddasslem17  33923  paddass  33925  padd12N  33926  paddssw1  33930  pmodlem2  33934  pmodN  33937  pmapjlln1  33942  atmod1i2  33946  pexmidlem2N  34058  pexmidlem7N  34063  pl42lem2N  34067  pl42lem3N  34068  pl42lem4N  34069  pl42N  34070  lhp2lt  34088  lhpm0atN  34116  lautlt  34178  lautcvr  34179  lautj  34180  lautm  34181  ltrneq2  34235  cdleme1b  34314  cdleme3b  34317  cdleme3c  34318  cdleme9b  34340  cdlemefs27cl  34502  cdleme42mN  34576  cdlemg4c  34701  trljco  34829  tgrpgrplem  34838  tendoplass  34872  tendodi1  34873  tendodi2  34874  erngplus2  34893  erngplus2-rN  34901  cdlemk36  35002  erngdvlem3  35079  erngdvlem3-rN  35087  dvaplusgv  35099  tendospass  35109  tendospdi1  35110  dvalveclem  35115  dialss  35136  dvhvaddass  35187  dvhopvsca  35192  dvhlveclem  35198  diblss  35260  diclss  35283  diclspsn  35284  cdlemn11pre  35300  dihmeetlem12N  35408  dihmeetlem16N  35412  dihmeetlem17N  35413  dvh4dimN  35537  lpolsatN  35578  lpolpolsatN  35579  dochpolN  35580  lclkr  35623  lclkrs  35629  lcfr  35675  irrapxlem6  36192  jm2.26lem3  36369  mpaamn  36528  mendring  36564  mendlmod  36565  mendassa  36566  neicvgel1  37220  rfcnpre4  37999  fmuldfeq  38433  stoweidlem43  38719  stoweidlem52  38728  stoweidlem53  38729  stoweidlem56  38732  issmfgt  39426  issmfge  39439  iccelpart  39755  fmtnoprmfac1  39799  fmtnoprmfac2  39801  pfxccat3a  40076  funopsn  40123  structiedg0val  40236  subgruhgredgd  40489  upgrwlkdvde  40924  crctcsh1wlkn0lem5  40998  crctcsh1wlkn0  41005  umgrwwlks2on  41142  rusgrnumwwlks  41158  rusgrnumwlkg  41161  3spthd  41324  av-numclwwlk5  41523  av-friendship  41534  copissgrp  41579  ringrng  41650  cznrng  41728  funcringcsetcALTV2lem9  41817  funcringcsetclem9ALTV  41840  linccl  41978  lincsumscmcl  41997  ldepsprlem  42036  lincresunit3lem1  42043
  Copyright terms: Public domain W3C validator