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

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

Proof of Theorem simpl2
StepHypRef Expression
1 simp2 1054 . 2 ((𝜑𝜓𝜒) → 𝜓)
21adantr 479 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:  simpll2  1093  simprl2  1099  simp1l2  1147  simp2l2  1153  simp3l2  1159  3anandirs  1426  rspc3ev  3296  f1prex  6416  weniso  6481  ofmpteq  6791  tfisi  6927  mpt2sn  7132  smogt  7328  smorndom  7329  omeulem1  7526  nnmord  7576  nnmword  7577  difsnen  7904  enfixsn  7931  mapunen  7991  ac6sfi  8066  ordiso2  8280  wemaplem2  8312  wemapso  8316  wemapso2lem  8317  en2eqpr  8690  acndom  8734  infmap2  8900  cflim2  8945  cfsmolem  8952  coftr  8955  fin23lem26  9007  isf32lem9  9043  fin1a2lem9  9090  fin1a2lem10  9091  ac6num  9161  gchdomtri  9307  canth4  9325  gchpwdom  9348  gruima  9480  grudomon  9495  prn0  9667  distrlem4pr  9704  prlem934  9711  addcan  10071  addcan2  10072  divmulass  10559  divmulasscom  10560  ltmul1a  10723  supmul1  10841  uzsupss  11614  xaddass  11910  xleadd1a  11914  xlesubadd  11924  xmulass  11948  xlemul2a  11950  xadddilem  11955  xadddi  11956  ixxdisj  12019  ixxun  12020  ixxlb  12026  icoshftf1o  12124  icodisj  12126  lincmb01cmp  12144  iccf1o  12145  ssfzoulel  12385  modmuladd  12531  modaddmulmod  12556  ltexp2a  12731  leexp2  12734  ltexp2r  12736  exple1  12739  expnlbnd2  12814  mulsubdivbinom2  12865  ccatass  13172  ccatopth  13270  swrdccatin12lem2a  13284  repswccat  13331  cshwidxmodr  13349  2cshw  13358  repsco  13384  s2f1o  13459  limsupgle  14004  limsupgre  14008  addcn2  14120  mulcn2  14122  binomrisefac  14560  dvdsval2  14772  dvdsadd2b  14814  dvdsmod  14836  oexpneg  14855  sadass  14979  gcdass  15050  rplpwr  15062  rppwr  15063  lcmass  15113  coprmdvds2  15154  rpmulgcd2  15156  rpdvds  15160  coprmprod  15161  cncongr2  15168  rpexp  15218  prmdiveq  15277  hashgcdlem  15279  odzdvds  15286  coprimeprodsq2  15300  pythagtriplem3  15309  pythagtriplem4  15310  pcdvdsb  15359  vdwnnlem1  15485  0ram  15510  ramz2  15514  ramub1lem1  15516  mremre  16035  mrieqv2d  16070  lubss  16892  lubun  16894  clatleglb  16897  clatglbss  16898  mrelatglb  16955  isnsgrp  17059  issubmnd  17089  gsumccat  17149  frmdss2  17171  nmzsubg  17406  ghmnsgima  17455  gsmsymgreqlem1  17621  psgnunilem4  17688  odmodnn0  17730  odnncl  17735  odmod  17736  oddvds  17737  odeq  17740  odmulgid  17742  odmulgeq  17745  odbezout  17746  odf1o1  17758  odf1o2  17759  odngen  17763  gexdvdsi  17769  pgpfi1  17781  odcau  17790  subgslw  17802  fislw  17811  lsmless1x  17830  lsmless2x  17831  lsmsubm  17839  lsmmod  17859  lsmmod2  17860  efgsfo  17923  odadd1  18022  odadd2  18023  odadd  18024  lsmcomx  18030  prdscmnd  18035  gsumconst  18105  srg1zr  18300  csrgbinom  18317  ring1eq0  18361  mulgass2  18372  cntzsubr  18583  isabvd  18591  0lmhm  18809  lmhmvsca  18814  reslmhm2b  18823  pwssplit1  18828  pwssplit2  18829  pwssplit3  18830  lbspss  18851  lspsnat  18914  lidldvgen  19024  issubassa  19093  evlsval2  19289  coe1subfv  19405  coe1sclmul  19421  coe1sclmul2  19423  xrsdsreclblem  19559  cssmre  19803  obs2ss  19839  uvcresum  19898  frlmsslsp  19901  frlmup4  19906  lindff1  19925  f1lindf  19927  lsslindf  19935  islindf4  19943  mpt2matmul  20018  mamutpos  20030  scmatscmide  20079  mavmulsolcl  20123  mulmarep1gsum2  20146  mdetdiaglem  20170  mdetdiag  20171  mdetunilem1  20184  mdetunilem3  20186  mdetunilem9  20192  maducoeval2  20212  madurid  20216  slesolinvbi  20253  cramerimplem1  20255  cramerlem1  20259  cramer  20263  cpmatel2  20284  m2cpm  20312  m2pmfzmap  20318  m2cpminvid2lem  20325  m2cpminvid2  20326  decpmatmul  20343  pmatcollpw1lem2  20346  pmatcollpw1  20347  pmatcollpw2lem  20348  pmatcollpwfi  20353  pm2mpcl  20368  mply1topmatcl  20376  mp2pm2mplem2  20378  mp2pm2mplem4  20380  mp2pm2mplem5  20381  mp2pm2mp  20382  pm2mpghmlem2  20383  pm2mpghmlem1  20384  chfacfisfcpmat  20426  topssnei  20685  cnconst2  20844  cnpresti  20849  cnprest2  20851  cnpdis  20854  cnt0  20907  cnt1  20911  cnhaus  20915  sscmp  20965  hauscmp  20967  cnconn  20982  uncon  20989  finlocfin  21080  comppfsc  21092  kgen2ss  21115  ptpjopn  21172  prdstopn  21188  ptrescn  21199  qtopss  21275  kqfvima  21290  fbssint  21399  fbasrn  21445  filuni  21446  fmss  21507  rnelfm  21514  fmufil  21520  fmco  21522  flimss2  21533  flimss1  21534  flimrest  21544  cnpflf2  21561  flfcnp  21565  supnfcls  21581  fclsss1  21583  fclsss2  21584  isfcf  21595  subgntr  21667  opnsubg  21668  cldsubg  21671  ghmcnp  21675  ustuqtop1  21802  bldisj  21960  blgt0  21961  bl2in  21962  blss2ps  21965  blss2  21966  blssps  21986  blss  21987  xmetresbl  21999  lpbl  22065  blcld  22067  stdbdmopn  22080  metcnp3  22102  metcnp  22103  metcnp2  22104  txmetcnp  22109  blval2  22124  nmoix  22290  nmoi2  22291  nmotri  22300  metdsge  22407  metdseq0  22412  iocopnst  22494  xrhmeo  22500  nmhmcn  22675  cphsqrtcl2  22738  cphsqrtcl3  22739  pjth  22962  ovoliunlem2  23022  volun  23064  mbfimaopn2  23174  iblconst  23334  limcvallem  23385  dvfval  23411  dvcnp2  23433  dvcn  23434  deg1mul3le  23624  deg1tmle  23625  dvdsq1p  23668  ig1peu  23679  ig1pdvds  23684  ply1term  23708  coeid3  23744  dgrmulc  23775  dvply1  23787  aaliou2  23843  efcvx  23951  tanord  24032  eflogeq  24096  logdivlti  24114  logccv  24153  recxpcl  24165  cxplea  24186  cxpeq  24242  ang180  24288  isosctrlem2  24293  cxp2lim  24447  amgm  24461  muval1  24603  dvdssqf  24608  mumullem2  24650  mumul  24651  bcmono  24746  lgsneg  24790  lgsdilem  24793  lgsdirprm  24800  lgsdir  24801  lgsdi  24803  lgsne0  24804  brbtwn2  25530  colinearalglem1  25531  colinearalg  25535  axcgrtr  25540  axsegconlem8  25549  axsegconlem9  25550  axsegconlem10  25551  axcontlem2  25590  axcontlem10  25598  cyclispthon  25954  wwlknext  26045  clwlkisclwwlklem0  26109  erclwwlksym  26135  eleclclwwlknlem2  26139  erclwwlkneqlen  26145  erclwwlknsym  26147  vdgrfval  26215  nbhashuvtx1  26235  usgreghash2spot  26389  extwwlkfablem2  26398  numclwwlk3lem  26428  frgraregord13  26439  nvmul0or  26682  ipval2lem2  26736  lnoadd  26790  lnosub  26791  lnomul  26792  shless  27395  shlej1  27396  kbmul  27991  homco2  28013  kbass2  28153  eliccelico  28722  elicoelioo  28723  iocinioc2  28724  iocinif  28726  difioo  28727  xrge0adddir  28816  xrge0npcan  28818  isarchi2  28863  archiabl  28876  rhmdvdsr  28942  pstmfval  29060  fmcncfil  29098  zrhnm  29134  qqhnm  29155  nexple  29192  volfiniune  29413  dya2iocnrect  29463  probinc  29603  cndprob01  29617  signswmnd  29753  bnj517  30002  cvmsss2  30303  cvmlift2lem10  30341  br6  30693  funsseq  30705  frrlem4  30820  cgrtriv  31072  5segofs  31076  btwnouttr2  31092  btwnxfr  31126  lineext  31146  btwnconn1lem13  31169  brsegle2  31179  nn0prpwlem  31280  lindsenlbs  32357  blbnd  32539  ismtyima  32555  rrndstprj2  32583  ghomdiv  32644  grpokerinj  32645  lsatfixedN  33097  lssat  33104  lshpkrlem4  33201  cvrcon3b  33365  atlen0  33398  atcvreq0  33402  atnle  33405  atlatmstc  33407  atlatle  33408  cvlcvr1  33427  hlsupr2  33474  hlrelat2  33490  cvrexchlem  33506  lnnat  33514  atcvrj2b  33519  3dimlem3  33548  3dim1  33554  1cvrjat  33562  llni  33595  llni2  33599  llnexatN  33608  2llnmat  33611  lplni  33619  2atnelpln  33631  llncvrlpln2  33644  2llnmj  33647  lplnexatN  33650  lplnexllnN  33651  2llnm3N  33656  lvoli  33662  lvoli3  33664  lvolnle3at  33669  islvol2aN  33679  4atlem4a  33686  4atlem4b  33687  4atlem11  33696  lplncvrlvol2  33702  2lplnmj  33709  islinei  33827  linepmap  33862  lnjatN  33867  lncvrat  33869  lncmp  33870  elpaddn0  33887  elpaddatriN  33890  elpaddat  33891  paddcom  33900  paddss2  33905  paddss12  33906  paddasslem4  33910  paddasslem9  33915  paddasslem10  33916  pmodl42N  33938  pmapjoin  33939  llnmod1i2  33947  polcon2bN  34007  pclfinclN  34037  poml4N  34040  poml6N  34042  osumcllem1N  34043  osumcllem2N  34044  osumcllem11N  34053  osumclN  34054  pmapojoinN  34055  pexmidlem2N  34058  pexmidlem3N  34059  pexmidlem4N  34060  pexmidlem6N  34062  pexmidlem7N  34063  pl42lem2N  34067  pl42lem3N  34068  pl42lem4N  34069  pl42N  34070  lhprelat3N  34127  4atex  34163  lauteq  34182  lautco  34184  ltrncoidN  34215  ltrneq2  34235  ltrnideq  34263  trlnle  34274  trlval3  34275  cdlemc  34285  cdlemd9  34294  cdlemd  34295  cdleme21j  34425  cdleme21  34426  cdleme29ex  34463  cdlemefr27cl  34492  cdlemefs27cl  34502  cdleme32d  34533  cdleme32f  34535  cdleme35h2  34546  cdleme40m  34556  cdleme17d3  34585  cdleme48fvg  34589  cdlemeg46fvcl  34595  cdlemeg46fgN  34623  cdleme48fgv  34627  cdleme50trn3  34642  cdlemb3  34695  cdlemg8  34720  cdlemg11a  34726  cdlemg15a  34744  cdlemg15  34745  cdlemg16  34746  cdlemg16z  34748  cdlemg17dN  34752  cdlemg24  34777  cdlemg37  34778  cdlemg29  34794  cdlemg33b  34796  cdlemg38  34804  cdlemg40  34806  trlco  34816  cdlemg44b  34821  ltrncom  34827  trljco  34829  tendococl  34861  tendoplcl  34870  tendoplcom  34871  cdlemj2  34911  tendoid0  34914  tendo1ne0  34917  cdlemk25-3  34993  cdlemk36  35002  cdlemkid4  35023  cdlemk19x  35032  cdlemk53  35046  cdlemk56  35060  cdleml5N  35069  tendospcanN  35113  cdlemm10N  35208  dihord6apre  35346  dihord  35354  dihmeetlem1N  35380  dihglblem2N  35384  dihmeetlem2N  35389  dihmeetbN  35393  dihmeetlem5  35398  dihmeetlem6  35399  dihmeetlem7N  35400  dihmeetlem10N  35406  dihmeetlem12N  35408  dihmeetlem16N  35412  dihmeetlem17N  35413  dihmeetlem18N  35414  dihmeetALTN  35417  dihlspsnssN  35422  dvh3dim2  35538  dvh3dim3N  35539  lcfrlem16  35648  mapdrvallem2  35735  mapdh8ad  35869  hgmapvvlem3  36018  diophrw  36123  eldioph2lem1  36124  diophrex  36140  rencldnfi  36186  pellexlem2  36195  pellqrexplicit  36242  infmrgelbi  36243  pellfundglb  36250  pellfund14gap  36252  rmxycomplete  36283  congadd  36334  acongeq  36351  jm2.19  36361  jm2.23  36364  jm2.20nn  36365  jm2.27  36376  jm3.1  36388  lnmepi  36456  lmhmlnmsplit  36458  hbtlem2  36496  dgraa0p  36521  idomrootle  36575  proot1hash  36580  iocunico  36598  iocinico  36599  relexpxpmin  36811  ntrclsk3  37171  rfcnnnub  38001  uzwo4  38029  supxrge  38278  infleinflem2  38311  snunioo2  38361  iccintsng  38379  climsuse  38458  lptre2pt  38490  limcleqr  38494  0ellimcdiv  38499  fnlimfvre  38524  dvnprodlem1  38619  volioc  38647  stoweidlem17  38693  stoweidlem19  38695  stoweidlem20  38696  stoweidlem22  38698  stoweidlem28  38704  stoweidlem34  38710  stoweidlem44  38720  stoweidlem60  38736  wallispilem3  38743  fourierdlem42  38825  fourierdlem48  38830  fourierdlem51  38833  fourierdlem54  38836  fourierdlem74  38856  fourierdlem77  38859  fourierdlem87  38869  fourierdlem97  38879  ioorrnopnlem  38983  ovnsubaddlem2  39244  fzopredsuc  39730  lighneallem4  39849  oexpnegALTV  39910  oexpnegnz  39911  tgblthelfgott  40013  tgblthelfgottOLD  40020  repswpfx  40083  fun2dmnop0  40133  eluzge0nn0  40156  fzoopth  40166  ewlkle  40788  edginwlk  40820  usgr2trlncl  40947  crctcsh1wlkn0lem5  40998  wwlknp  41026  1wlkiswwlks1  41045  wwlksnext  41080  wspthsnwspthsnon  41103  clwlkclwwlklem3  41191  erclwwlkssym  41223  erclwwlksnsym  41235  upgriseupth  41356  eucrct2eupth  41394  3cyclfrgrrn  41437  av-frgraregord13  41531  rmsupp0  41924  rmsuppss  41926  lincresunit3lem3  42038  lincresunit3lem2  42044  lindssnlvec  42050  fdivmptf  42114  refdivmptf  42115  elbigolo1  42130
  Copyright terms: Public domain W3C validator