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

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

Proof of Theorem simpl2
StepHypRef Expression
1 simp2 1082 . 2 ((𝜑𝜓𝜒) → 𝜓)
21adantr 480 1 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054
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 197  df-an 385  df-3an 1056
This theorem is referenced by:  simpll2  1121  simprl2  1127  simp1l2  1175  simp2l2  1181  simp3l2  1187  3anandirs  1475  rspc3ev  3357  f1prex  6579  weniso  6644  ofmpteq  6958  tfisi  7100  mpt2sn  7313  smogt  7509  smorndom  7510  omeulem1  7707  nnmord  7757  nnmword  7758  difsnen  8083  enfixsn  8110  mapunen  8170  ac6sfi  8245  ordiso2  8461  wemaplem2  8493  wemapso  8497  wemapso2lem  8498  en2eqpr  8868  acndom  8912  infmap2  9078  cflim2  9123  cfsmolem  9130  coftr  9133  fin23lem26  9185  isf32lem9  9221  fin1a2lem9  9268  fin1a2lem10  9269  ac6num  9339  gchdomtri  9489  canth4  9507  gchpwdom  9530  gruima  9662  grudomon  9677  prn0  9849  distrlem4pr  9886  prlem934  9893  addcan  10258  addcan2  10259  divmulass  10746  divmulasscom  10747  ltmul1a  10910  supmul1  11030  uzsupss  11818  xaddass  12117  xleadd1a  12121  xlesubadd  12131  xmulass  12155  xlemul2a  12157  xadddilem  12162  xadddi  12163  ixxdisj  12228  ixxun  12229  ixxlb  12235  icoshftf1o  12333  icodisj  12335  lincmb01cmp  12353  iccf1o  12354  elfz1b  12447  ssfzoulel  12602  modmuladd  12752  modaddmulmod  12777  ltexp2a  12952  leexp2  12955  ltexp2r  12957  exple1  12960  expnlbnd2  13035  mulsubdivbinom2  13086  fun2dmnop0  13314  ccatass  13406  ccatopth  13516  swrdccatin12lem2a  13531  repswccat  13578  cshwidxmodr  13596  2cshw  13605  repsco  13631  s2f1o  13707  limsupgle  14252  limsupgre  14256  addcn2  14368  mulcn2  14370  binomrisefac  14817  dvdsval2  15030  dvdsadd2b  15075  dvdsmod  15097  oexpneg  15116  sadass  15240  gcdass  15311  rplpwr  15323  rppwr  15324  lcmass  15374  coprmdvds2  15415  rpmulgcd2  15417  rpdvds  15421  coprmprod  15422  cncongr2  15429  rpexp  15479  prmdiveq  15538  hashgcdlem  15540  odzdvds  15547  coprimeprodsq2  15561  pythagtriplem3  15570  pythagtriplem4  15571  pcdvdsb  15620  vdwnnlem1  15746  0ram  15771  ramz2  15775  ramub1lem1  15777  mremre  16311  mrieqv2d  16346  lubss  17168  lubun  17170  clatleglb  17173  clatglbss  17174  mrelatglb  17231  isnsgrp  17335  issubmnd  17365  gsumccat  17425  frmdss2  17447  nmzsubg  17682  ghmnsgima  17731  gsmsymgreqlem1  17896  psgnunilem4  17963  odmodnn0  18005  odnncl  18010  odmod  18011  oddvds  18012  odeq  18015  odmulgid  18017  odmulgeq  18020  odbezout  18021  odf1o1  18033  odf1o2  18034  odngen  18038  gexdvdsi  18044  pgpfi1  18056  odcau  18065  subgslw  18077  fislw  18086  lsmless1x  18105  lsmless2x  18106  lsmsubm  18114  lsmmod  18134  lsmmod2  18135  efgsfo  18198  odadd1  18297  odadd2  18298  odadd  18299  lsmcomx  18305  prdscmnd  18310  gsumconst  18380  srg1zr  18575  csrgbinom  18592  ring1eq0  18636  mulgass2  18647  cntzsubr  18860  isabvd  18868  rmodislmod  18979  0lmhm  19088  lmhmvsca  19093  reslmhm2b  19102  pwssplit1  19107  pwssplit2  19108  pwssplit3  19109  lbspss  19130  lspsnat  19193  lidldvgen  19303  issubassa  19372  evlsval2  19568  coe1subfv  19684  coe1sclmul  19700  coe1sclmul2  19702  xrsdsreclblem  19840  cssmre  20085  obs2ss  20121  uvcresum  20180  frlmsslsp  20183  frlmup4  20188  lindff1  20207  f1lindf  20209  lsslindf  20217  islindf4  20225  mpt2matmul  20300  mamutpos  20312  scmatscmide  20361  mavmulsolcl  20405  mulmarep1gsum2  20428  mdetdiaglem  20452  mdetdiag  20453  mdetunilem1  20466  mdetunilem3  20468  mdetunilem9  20474  maducoeval2  20494  madurid  20498  slesolinvbi  20535  cramerimplem1  20537  cramerlem1  20541  cramer  20545  cpmatel2  20566  m2cpm  20594  m2pmfzmap  20600  m2cpminvid2lem  20607  m2cpminvid2  20608  decpmatmul  20625  pmatcollpw1lem2  20628  pmatcollpw1  20629  pmatcollpw2lem  20630  pmatcollpwfi  20635  pm2mpcl  20650  mply1topmatcl  20658  mp2pm2mplem2  20660  mp2pm2mplem4  20662  mp2pm2mplem5  20663  mp2pm2mp  20664  pm2mpghmlem2  20665  pm2mpghmlem1  20666  chfacfisfcpmat  20708  topssnei  20976  cnconst2  21135  cnpresti  21140  cnprest2  21142  cnpdis  21145  cnt0  21198  cnt1  21202  cnhaus  21206  sscmp  21256  hauscmp  21258  cnconn  21273  unconn  21280  finlocfin  21371  comppfsc  21383  kgen2ss  21406  ptpjopn  21463  prdstopn  21479  ptrescn  21490  qtopss  21566  kqfvima  21581  fbssint  21689  fbasrn  21735  filuni  21736  fmss  21797  rnelfm  21804  fmufil  21810  fmco  21812  flimss2  21823  flimss1  21824  flimrest  21834  cnpflf2  21851  flfcnp  21855  supnfcls  21871  fclsss1  21873  fclsss2  21874  isfcf  21885  subgntr  21957  opnsubg  21958  cldsubg  21961  ghmcnp  21965  ustuqtop1  22092  bldisj  22250  blgt0  22251  bl2in  22252  blss2ps  22255  blss2  22256  blssps  22276  blss  22277  xmetresbl  22289  lpbl  22355  blcld  22357  stdbdmopn  22370  metcnp3  22392  metcnp  22393  metcnp2  22394  txmetcnp  22399  blval2  22414  nmoix  22580  nmoi2  22581  nmotri  22590  metdsge  22699  metdseq0  22704  iocopnst  22786  xrhmeo  22792  nmhmcn  22966  cphsqrtcl2  23032  cphsqrtcl3  23033  pjth  23256  ovoliunlem2  23317  volun  23359  mbfimaopn2  23469  iblconst  23629  limcvallem  23680  dvfval  23706  dvcnp2  23728  dvcn  23729  deg1mul3le  23921  deg1tmle  23922  dvdsq1p  23965  ig1peu  23976  ig1pdvds  23981  ply1term  24005  coeid3  24041  dgrmulc  24072  dvply1  24084  aaliou2  24140  efcvx  24248  tanord  24329  eflogeq  24393  logdivlti  24411  logccv  24454  recxpcl  24466  cxplea  24487  cxpeq  24543  ang180  24589  isosctrlem2  24594  cxp2lim  24748  amgm  24762  muval1  24904  dvdssqf  24909  mumullem2  24951  mumul  24952  bcmono  25047  lgsneg  25091  lgsdilem  25094  lgsdirprm  25101  lgsdir  25102  lgsdi  25104  lgsne0  25105  brbtwn2  25830  colinearalglem1  25831  colinearalg  25835  axcgrtr  25840  axsegconlem8  25849  axsegconlem9  25850  axsegconlem10  25851  axcontlem2  25890  axcontlem10  25898  ewlkle  26557  edginwlkOLD  26587  crctcshwlkn0lem5  26762  wwlknp  26791  wwlksnext  26856  wwlksnextproplem1  26872  wspthsnwspthsnon  26879  wspthsnwspthsnonOLD  26881  clwlkclwwlklem3  26967  erclwwlksym  26978  erclwwlknsym  27034  clwwlknonex2lem2  27083  upgriseupth  27185  eucrct2eupth  27223  3cyclfrgrrn  27266  numclwwlk2lem1lem  27324  numclwlk1lem2foa  27344  frgrregord13  27383  nvmul0or  27633  ipval2lem2  27687  lnoadd  27741  lnosub  27742  lnomul  27743  shless  28346  shlej1  28347  kbmul  28942  homco2  28964  kbass2  29104  eliccelico  29667  elicoelioo  29668  iocinioc2  29669  iocinif  29671  difioo  29672  xrge0adddir  29820  xrge0npcan  29822  isarchi2  29867  archiabl  29880  rhmdvdsr  29946  pstmfval  30067  fmcncfil  30105  zrhnm  30141  qqhnm  30162  nexple  30199  volfiniune  30421  dya2iocnrect  30471  probinc  30611  cndprob01  30625  signswmnd  30762  bnj517  31081  cvmsss2  31382  cvmlift2lem10  31420  br6  31773  funsseq  31792  nolesgn2o  31949  nosep1o  31957  nosepssdm  31961  nosupres  31978  nosupbnd1lem1  31979  nosupbnd1lem4  31982  nosupbnd1lem5  31983  nosupbnd1lem6  31984  noetalem2  31989  cgrtriv  32234  5segofs  32238  btwnouttr2  32254  btwnxfr  32288  lineext  32308  btwnconn1lem13  32331  brsegle2  32341  nn0prpwlem  32442  lindsenlbs  33534  blbnd  33716  ismtyima  33732  rrndstprj2  33760  ghomdiv  33821  grpokerinj  33822  lsatfixedN  34614  lssat  34621  lshpkrlem4  34718  cvrcon3b  34882  atlen0  34915  atcvreq0  34919  atnle  34922  atlatmstc  34924  atlatle  34925  cvlcvr1  34944  hlsupr2  34991  hlrelat2  35007  cvrexchlem  35023  lnnat  35031  atcvrj2b  35036  3dimlem3  35065  3dim1  35071  1cvrjat  35079  llni  35112  llni2  35116  llnexatN  35125  2llnmat  35128  lplni  35136  2atnelpln  35148  llncvrlpln2  35161  2llnmj  35164  lplnexatN  35167  lplnexllnN  35168  2llnm3N  35173  lvoli  35179  lvoli3  35181  lvolnle3at  35186  islvol2aN  35196  4atlem4a  35203  4atlem4b  35204  4atlem11  35213  lplncvrlvol2  35219  2lplnmj  35226  islinei  35344  linepmap  35379  lnjatN  35384  lncvrat  35386  lncmp  35387  elpaddn0  35404  elpaddatriN  35407  elpaddat  35408  paddcom  35417  paddss2  35422  paddss12  35423  paddasslem4  35427  paddasslem9  35432  paddasslem10  35433  pmodl42N  35455  pmapjoin  35456  llnmod1i2  35464  polcon2bN  35524  pclfinclN  35554  poml4N  35557  poml6N  35559  osumcllem1N  35560  osumcllem2N  35561  osumcllem11N  35570  osumclN  35571  pmapojoinN  35572  pexmidlem2N  35575  pexmidlem3N  35576  pexmidlem4N  35577  pexmidlem6N  35579  pexmidlem7N  35580  pl42lem2N  35584  pl42lem3N  35585  pl42lem4N  35586  pl42N  35587  lhprelat3N  35644  4atex  35680  lauteq  35699  lautco  35701  ltrncoidN  35732  ltrneq2  35752  ltrnideq  35780  trlnle  35791  trlval3  35792  cdlemc  35802  cdlemd9  35811  cdlemd  35812  cdleme21j  35941  cdleme21  35942  cdleme29ex  35979  cdlemefr27cl  36008  cdlemefs27cl  36018  cdleme32d  36049  cdleme32f  36051  cdleme35h2  36062  cdleme40m  36072  cdleme17d3  36101  cdleme48fvg  36105  cdlemeg46fvcl  36111  cdlemeg46fgN  36139  cdleme48fgv  36143  cdleme50trn3  36158  cdlemb3  36211  cdlemg8  36236  cdlemg11a  36242  cdlemg15a  36260  cdlemg15  36261  cdlemg16  36262  cdlemg16z  36264  cdlemg17dN  36268  cdlemg24  36293  cdlemg37  36294  cdlemg29  36310  cdlemg33b  36312  cdlemg38  36320  cdlemg40  36322  trlco  36332  cdlemg44b  36337  ltrncom  36343  trljco  36345  tendococl  36377  tendoplcl  36386  tendoplcom  36387  cdlemj2  36427  tendoid0  36430  tendo1ne0  36433  cdlemk25-3  36509  cdlemk36  36518  cdlemkid4  36539  cdlemk19x  36548  cdlemk53  36562  cdlemk56  36576  cdleml5N  36585  tendospcanN  36629  cdlemm10N  36724  dihord6apre  36862  dihord  36870  dihmeetlem1N  36896  dihglblem2N  36900  dihmeetlem2N  36905  dihmeetbN  36909  dihmeetlem5  36914  dihmeetlem6  36915  dihmeetlem7N  36916  dihmeetlem10N  36922  dihmeetlem12N  36924  dihmeetlem16N  36928  dihmeetlem17N  36929  dihmeetlem18N  36930  dihmeetALTN  36933  dihlspsnssN  36938  dvh3dim2  37054  dvh3dim3N  37055  lcfrlem16  37164  mapdrvallem2  37251  mapdh8ad  37385  hgmapvvlem3  37534  diophrw  37639  eldioph2lem1  37640  diophrex  37656  rencldnfi  37702  pellexlem2  37711  pellqrexplicit  37758  infmrgelbi  37759  pellfundglb  37766  pellfund14gap  37768  rmxycomplete  37799  congadd  37850  acongeq  37867  jm2.19  37877  jm2.23  37880  jm2.20nn  37881  jm2.27  37892  jm3.1  37904  lnmepi  37972  lmhmlnmsplit  37974  hbtlem2  38011  dgraa0p  38036  idomrootle  38090  proot1hash  38095  iocunico  38113  iocinico  38114  relexpxpmin  38326  ntrclsk3  38685  rfcnnnub  39509  uzwo4  39535  supxrge  39867  infleinflem2  39900  snunioo2  40049  iccintsng  40067  climsuse  40158  lptre2pt  40190  limcleqr  40194  0ellimcdiv  40199  fnlimfvre  40224  dvnprodlem1  40479  volioc  40506  stoweidlem17  40552  stoweidlem19  40554  stoweidlem20  40555  stoweidlem22  40557  stoweidlem28  40563  stoweidlem34  40569  stoweidlem44  40579  stoweidlem60  40595  wallispilem3  40602  fourierdlem42  40684  fourierdlem48  40689  fourierdlem51  40692  fourierdlem54  40695  fourierdlem74  40715  fourierdlem77  40718  fourierdlem87  40728  fourierdlem97  40738  ioorrnopnlem  40842  ovnsubaddlem2  41106  smfinflem  41344  eluzge0nn0  41647  fzopredsuc  41658  fzoopth  41662  repswpfx  41761  lighneallem4  41852  oexpnegALTV  41913  oexpnegnz  41914  tgblthelfgott  42028  tgblthelfgottOLD  42034  rmsupp0  42474  rmsuppss  42476  lincresunit3lem3  42588  lincresunit3lem2  42594  lindssnlvec  42600  fdivmptf  42660  refdivmptf  42661  elbigolo1  42676
  Copyright terms: Public domain W3C validator