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

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

Proof of Theorem simpl1
StepHypRef Expression
1 simp1 1053 . 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:  simpll1  1092  simprl1  1098  simp1l1  1146  simp2l1  1152  simp3l1  1158  3anandirs  1426  rspc3ev  3296  f1prex  6416  cocan1  6423  weniso  6481  smogt  7328  smorndom  7329  omeulem1  7526  nnmord  7576  nnmword  7577  difsnen  7904  enfixsn  7931  mapunen  7991  ac6sfi  8066  fipreima  8132  elfiun  8196  ordiso2  8280  wemaplem2  8312  wemapso  8316  en2eqpr  8690  indcardi  8724  fodomfi2  8743  iunfictbso  8797  infmap2  8900  cofsmo  8951  cfsmolem  8952  coftr  8955  fin23lem11  8999  fincssdom  9005  fin23lem26  9007  isf32lem9  9043  ac6num  9161  gchdomtri  9307  gchpwdom  9348  winainflem  9371  tskuni  9461  gruima  9480  gruf  9489  grudomon  9495  elnpi  9666  distrlem4pr  9704  prlem934  9711  addcan  10071  addcan2  10072  divmulass  10559  divmulasscom  10560  ltmul1a  10723  suprleub  10838  supmul1  10841  suprzcl  11291  uzsupss  11614  xleadd1a  11914  xlesubadd  11924  xmulasslem3  11947  xlemul2a  11950  xadddilem  11955  xadddi2  11958  ixxun  12020  icoshftf1o  12124  snunioc  12129  lincmb01cmp  12144  iccf1o  12145  nn0p1elfzo  12335  fzofzim  12339  ltexp2a  12731  leexp2  12734  ltexp2r  12736  exple1  12739  expnlbnd2  12814  ccatass  13172  ccat2s1fvw  13215  swrdswrdlem  13259  ccatopth  13270  cshimadifsn  13374  cshimadifsn0  13375  cshco  13381  repsco  13384  s2f1o  13459  limsupgre  14008  addcn2  14120  mulcn2  14122  ntrivcvgmul  14421  binomrisefac  14560  dvdsadd2b  14814  dvdsmod  14836  oexpneg  14855  sadass  14979  gcdass  15050  rplpwr  15062  rppwr  15063  lcmfunsnlem1  15136  coprmdvds2  15154  rpmulgcd2  15156  qredeq  15157  rpdvds  15160  cncongr2  15168  rpexp  15218  prmdiveq  15277  hashgcdlem  15279  odzdvds  15286  modprmn0modprm0  15298  coprimeprodsq2  15300  pythagtriplem3  15309  pcdvdsb  15359  pcgcd1  15367  qexpz  15391  pockthg  15396  vdwnnlem1  15485  0ram  15510  ramz2  15514  lubss  16892  lubun  16894  clatleglb  16897  clatglbss  16898  mrelatglb  16955  isnsgrp  17059  issubmnd  17089  ress0g  17090  gsumccat  17149  frmdss2  17171  mulgneg  17331  mulgdirlem  17343  submmulg  17357  subgmulg  17379  nmzsubg  17406  ghmmulg  17443  gsmsymgreqlem1  17621  pmtrfb  17656  psgnunilem4  17688  odmodnn0  17730  odnncl  17735  odmod  17736  odmulgid  17742  odmulgeq  17745  odf1o1  17758  odf1o2  17759  odngen  17763  gexdvdsi  17769  pgpfi1  17781  odcau  17790  subgslw  17802  fislw  17811  lsmssv  17829  lsmless1x  17830  lsmless2x  17831  lsmsubm  17839  lsmmod  17859  lsmmod2  17860  efgred  17932  cntzcmn  18016  ghmplusg  18020  odadd1  18022  odadd2  18023  odadd  18024  lsmcomx  18030  gsumconst  18105  srg1zr  18300  ring1eq0  18361  mulgass2  18372  isabvd  18591  lssintcl  18733  0lmhm  18809  lmhmvsca  18814  reslmhm2b  18823  pwssplit1  18828  pwssplit3  18830  lspfixed  18897  lspsnat  18914  lidldvgen  19024  issubassa  19093  evlsval2  19289  psrplusgpropd  19375  coe1subfv  19405  coe1mul2  19408  xrsdsreclblem  19559  regsumsupp  19734  obselocv  19838  uvcresum  19898  frlmsslsp  19901  frlmup4  19906  lindff1  19925  f1lindf  19927  lsslindf  19935  islindf4  19943  lbslcic  19946  mhmvlin  19969  mpt2matmul  20018  mamutpos  20030  scmatscmide  20079  mavmulsolcl  20123  marrepcl  20136  mdetdiag  20171  mdetunilem1  20184  mdetunilem3  20186  mdetunilem7  20190  mdetunilem9  20192  mdetmul  20195  slesolinvbi  20253  m2pmfzmap  20318  pmatcollpwlem  20351  pmatcollpw  20352  mp2pm2mplem4  20380  chpdmatlem3  20411  chfacfisfcpmat  20426  chfacfscmulgsum  20431  chfacfpmmulgsum  20435  chfacfpmmulgsum2  20436  cayhamlem1  20437  cpmidpmatlem2  20442  cpmadugsumlemB  20445  cpmadugsumlemC  20446  cpmadugsumlemF  20447  riinopn  20485  neiint  20665  topssnei  20685  restntr  20743  iscnp4  20824  cnconst2  20844  cnrest2  20847  cnprest2  20851  cnpdis  20854  cnt0  20907  cnt1  20911  cnhaus  20915  ordthauslem  20944  cncmp  20952  fiuncmp  20964  sscmp  20965  hauscmp  20967  cnconn  20982  uncon  20989  nlly2i  21036  llynlly  21037  nllyidm  21049  finlocfin  21080  ptrescn  21199  xkococnlem  21219  qtoptop2  21259  qtopss  21275  kqfvima  21290  r0cld  21298  ordthmeolem  21361  fbssint  21399  fmf  21506  fmss  21507  elfm  21508  rnelfmlem  21513  rnelfm  21514  fmco  21522  flimss2  21533  flimss1  21534  flimrest  21544  flftg  21557  cnpflf2  21561  cnpflf  21562  flfcnp  21565  supnfcls  21581  fclsss1  21583  fclsss2  21584  fcfnei  21596  fcfelbas  21597  cnpfcfi  21601  subgntr  21667  opnsubg  21668  cldsubg  21671  ghmcnp  21675  utop2nei  21811  neipcfilu  21857  bldisj  21960  blgt0  21961  bl2in  21962  blss2ps  21965  blss2  21966  blssps  21986  blss  21987  xmetresbl  21999  lpbl  22065  blcld  22067  stdbdbl  22079  metcnp3  22102  metcnp2  22104  txmetcnp  22109  blval2  22124  nmoix  22290  nmoeq0  22297  icoopnst  22493  iocopnst  22494  xrhmeo  22500  nmhmcn  22675  cphsqrtcl2  22738  cphsqrtcl3  22739  cfil3i  22819  caublcls  22859  bcthlem5  22877  cmetcusp1  22901  rrxcph  22932  pjth  22962  ovoliunlem2  23022  volun  23064  volsup2  23123  mbfimaopn2  23174  iblconst  23334  itgconst  23335  dvcnp2  23433  dvcn  23434  deg1mul3le  23624  deg1tmle  23625  dvdsq1p  23668  ig1peu  23679  ig1pdvds  23684  coeid3  23744  dgrmulc  23775  efcvx  23951  tanord  24032  logdivlti  24114  logccv  24153  recxpcl  24165  cxpeq  24242  ang180  24288  isosctrlem2  24293  cxp2lim  24447  amgm  24461  muval1  24603  dvdssqf  24608  mumullem2  24650  mumul  24651  bcmono  24746  lgsfcl2  24772  lgsdilem  24793  lgsdirprm  24800  lgsdir  24801  lgsdi  24803  lgsne0  24804  padicabv  25063  brbtwn2  25530  colinearalglem1  25531  colinearalg  25535  axcgrtr  25540  axsegconlem8  25549  axsegconlem9  25550  axsegconlem10  25551  axcontlem8  25596  axcontlem10  25598  2pthon  25925  clwwlkfo  26118  clwwlkext2edg  26123  erclwwlksym  26135  erclwwlknsym  26147  clwlkfoclwwlk  26165  clwlkf1clwwlklem  26169  numclwwlk2lem1  26422  numclwwlk5  26432  frgraregord13  26439  nvmul0or  26682  ipval2lem2  26736  lnomul  26792  shless  27395  shlej1  27396  pjspansn  27613  hoadddi  27839  kbmul  27991  homco2  28013  kbass2  28153  eliccelico  28722  elicoelioo  28723  iocinioc2  28724  iocinif  28726  xrge0adddir  28816  xrge0npcan  28818  archiabl  28876  ress1r  28913  rhmdvdsr  28942  pstmfval  29060  fmcncfil  29098  zrhnm  29134  qqhnm  29155  measvunilem  29395  volfiniune  29413  dya2iocnrect  29463  sibfinima  29521  probun  29601  probinc  29603  cndprob01  29617  bnj517  30002  bnj594  30029  pconpi1  30266  cvmsss2  30303  mrsubcv  30454  msubvrs  30504  dvdspw  30682  br6  30693  br4  30694  frrlem4  30820  cgrcomim  31059  cgrtriv  31072  cgrextend  31078  segconeq  31080  btwntriv2  31082  btwnintr  31089  btwnexch3  31090  btwnouttr2  31092  trisegint  31098  cgrsub  31115  cgrxfr  31125  btwnxfr  31126  lineext  31146  btwnconn1lem13  31169  btwnconn1lem14  31170  btwnconn3  31173  segcon2  31175  brsegle  31178  brsegle2  31179  segletr  31184  segleantisym  31185  seglelin  31186  outsideofeu  31201  lineunray  31217  lineelsb2  31218  ivthALT  31293  lindsenlbs  32357  areacirc  32458  cocanfo  32465  upixp  32477  ismtyima  32555  rrndstprj2  32583  zerdivemp1x  32699  lsatfixedN  33097  lssat  33104  eqlkr  33187  eqlkr2  33188  lkrlsp  33190  lshpkrlem4  33201  opposet  33269  cvrcon3b  33365  cvrcmp  33371  atlen0  33398  atnle  33405  atlatmstc  33407  cvlatexch3  33426  cvlsupr2  33431  hlsupr2  33474  hlrelat2  33490  cvrexchlem  33506  lnnat  33514  atcvrj2b  33519  atle  33523  atexchcvrN  33527  atbtwn  33533  athgt  33543  3dimlem3  33548  3dim1  33554  1cvratlt  33561  1cvrjat  33562  ps-1  33564  ps-2  33565  3atlem3  33572  3atlem5  33574  3atlem7  33576  llni  33595  llni2  33599  atcvrlln2  33606  llnexatN  33608  llncmp  33609  2llnmat  33611  2at0mat0  33612  lplni  33619  lplnnle2at  33628  2atnelpln  33631  lplnllnneN  33643  llncvrlpln2  33644  2lplnmN  33646  2llnmj  33647  lplncmp  33649  lplnexatN  33650  lplnexllnN  33651  2llnm3N  33656  lvoli  33662  lvoli3  33664  islvol2aN  33679  4atlem0a  33680  4atlem3  33683  4atlem3a  33684  4atlem4a  33686  4atlem4b  33687  4atlem4c  33688  4atlem4d  33689  4atlem10b  33692  4atlem11  33696  4atlem12  33699  lplncvrlvol2  33702  lvolcmp  33704  2lplnmj  33709  islinei  33827  pmapglbx  33856  linepmap  33862  lneq2at  33865  lnjatN  33867  lncvrat  33869  lncmp  33870  2llnma3r  33875  elpaddatriN  33890  elpaddat  33891  paddcom  33900  paddss1  33904  paddss2  33905  paddss12  33906  paddasslem6  33912  paddasslem7  33913  paddasslem8  33914  paddasslem9  33915  paddasslem15  33921  pmodlem2  33934  pmodl42N  33938  pmapjoin  33939  llnmod1i2  33947  2polcon4bN  34005  polcon2bN  34007  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  lhpexle2lem  34096  lhpexle3lem  34098  lhpexle3  34099  lhpmcvr3  34112  lhp2at0nle  34122  lhprelat3N  34127  4atex  34163  4atex2  34164  lauteq  34182  lautco  34184  ltrncoidN  34215  ltrneq2  34235  ltrnnidn  34262  ltrnideq  34263  trlnid  34267  ltrnatlw  34271  trlnle  34274  trlval3  34275  trlval4  34276  cdlemc  34285  cdlemd5  34290  cdlemd9  34294  ltrneq3  34296  cdleme0moN  34313  cdleme20  34413  cdleme21j  34425  cdleme21  34426  cdleme27cl  34455  cdlemefrs29bpre0  34485  cdlemefs27cl  34502  cdlemefs32sn1aw  34503  cdleme43fsv1snlem  34509  cdleme32d  34533  cdleme32f  34535  cdleme32le  34536  cdleme35h2  34546  cdleme38n  34553  cdleme40m  34556  cdleme41snaw  34565  cdleme42ke  34574  cdleme17d3  34585  cdleme48fvg  34589  cdlemeg46fvcl  34595  cdlemeg46fgN  34623  cdleme48gfv1  34625  cdleme48fgv  34627  cdleme50trn3  34642  trlord  34658  ltrniotavalbN  34673  cdlemb3  34695  cdlemg6c  34709  cdlemg6  34712  cdlemg7N  34715  cdlemg8c  34718  cdlemg8  34720  cdlemg11a  34726  cdlemg11b  34731  cdlemg12e  34736  cdlemg15a  34744  cdlemg15  34745  cdlemg16  34746  cdlemg16z  34748  cdlemg16zz  34749  cdlemg17dN  34752  cdlemg18a  34767  cdlemg20  34774  cdlemg22  34776  cdlemg24  34777  cdlemg37  34778  cdlemg31d  34789  cdlemg29  34794  cdlemg33b  34796  cdlemg33  34800  cdlemg38  34804  cdlemg39  34805  cdlemg40  34806  trlco  34816  trlcone  34817  cdlemg42  34818  cdlemg44b  34821  ltrncom  34827  trljco  34829  tendococl  34861  tendoplcl  34870  tendoplcom  34871  cdlemj2  34911  cdlemj3  34912  tendoid0  34914  tendoconid  34918  tendotr  34919  cdlemk25-3  34993  cdlemk26b-3  34994  cdlemk34  34999  cdlemk36  35002  cdlemk38  35004  cdlemkid4  35023  cdlemk35s-id  35027  cdlemk39s-id  35029  cdlemk19x  35032  cdlemk53  35046  cdlemk55  35050  cdlemk55u  35055  cdlemk39u  35057  cdlemk19u  35059  cdlemk56  35060  tendoex  35064  cdleml3N  35067  cdleml5N  35069  tendospcanN  35113  cdlemm10N  35208  cdlemn11pre  35300  dihord2pre  35315  dihvalcqpre  35325  dihopelvalcpre  35338  dihord6apre  35346  dihord5b  35349  dihord5apre  35352  dihord  35354  dihmeetlem1N  35380  dihglblem5apreN  35381  dihglblem3N  35385  dihmeetlem2N  35389  dihglbcpreN  35390  dihmeetbN  35393  dihmeetlem4preN  35396  dihmeetlem5  35398  dihmeetlem7N  35400  dihmeetlem10N  35406  dihmeetlem11N  35407  dihmeetlem12N  35408  dihmeetlem13N  35409  dihmeetlem15N  35411  dihmeetlem16N  35412  dihmeetlem17N  35413  dihmeetlem18N  35414  dihmeetlem19N  35415  dihmeetALTN  35417  dih1dimatlem0  35418  dihlspsnssN  35422  dihlspsnat  35423  mapdh8ad  35869  hdmap14lem14  35974  hgmapvvlem3  36018  mzprename  36113  eldioph2lem1  36124  lzunuz  36132  rencldnfi  36186  pellexlem2  36195  infmrgelbi  36243  pellfundglb  36250  pellfund14gap  36252  qirropth  36274  rmxycomplete  36283  congadd  36334  acongeq  36351  jm2.19  36361  jm2.23  36364  jm2.20nn  36365  jm2.27  36376  jm3.1  36388  aomclem6  36430  lnmepi  36456  lmhmfgsplit  36457  lmhmlnmsplit  36458  pwssplit4  36460  hbtlem2  36496  hbtlem5  36500  dgraa0p  36521  proot1hash  36580  iocunico  36598  relexpxpmin  36811  brtrclfv2  36821  ntrclsiso  37168  ntrclskb  37170  ntrclsk3  37171  k0004lem3  37250  suprnmpt  38133  wessf1ornlem  38149  projf1o  38164  snunioo2  38361  snunioo1  38368  iccintsng  38379  lptre2pt  38490  limcleqr  38494  fnlimfvre  38524  volioc  38647  iblspltprt  38648  stoweidlem19  38695  stoweidlem20  38696  stoweidlem22  38698  stoweidlem28  38704  stoweidlem34  38710  stoweidlem44  38720  stoweidlem60  38736  wallispilem3  38743  fourierdlem41  38824  fourierdlem42  38825  fourierdlem49  38831  fourierdlem51  38833  fourierdlem54  38836  fourierdlem74  38856  fourierdlem97  38879  caratheodorylem2  39200  ovnsubaddlem2  39244  hspmbllem2  39300  fzopredsuc  39730  iccpartigtl  39745  lighneal  39850  oexpnegALTV  39910  oexpnegnz  39911  tgblthelfgott  40013  tgblthelfgottOLD  40020  repswpfx  40083  fun2dmnop0  40133  fzoopth  40166  vtxdlfuhgr1v  40675  umgr2wlk  41137  clwwlksfo  41206  clwwlksext2edg  41211  erclwwlkssym  41223  erclwwlksnsym  41235  clwlksf1clwwlklem  41256  av-numclwwlk2lem1  41513  av-numclwwlk5  41523  av-frgraregord13  41531  lidldomn1  41692  ofaddmndmap  41896  lincdifsn  41988  lincellss  41990  lincresunit3lem3  42038  islindeps2  42047  lindssnlvec  42050  fdivmptf  42114  refdivmptf  42115
  Copyright terms: Public domain W3C validator