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

Theorem simpl1 960
Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
Assertion
Ref Expression
simpl1  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ph )

Proof of Theorem simpl1
StepHypRef Expression
1 simp1 957 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ph )
21adantr 452 1  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  simpll1  996  simprl1  1002  simp1l1  1050  simp2l1  1056  simp3l1  1062  3anandirs  1286  rspc3ev  3062  brcogw  5041  cocan1  6024  weniso  6075  smogt  6629  smorndom  6630  omeulem1  6825  nnmord  6875  nnmword  6876  difsnen  7190  mapunen  7276  ac6sfi  7351  fipreima  7412  elfiun  7435  ordiso2  7484  wemaplem2  7516  wemapso  7520  en2eqpr  7891  indcardi  7922  fodomfi2  7941  iunfictbso  7995  infmap2  8098  cofsmo  8149  cfsmolem  8150  coftr  8153  fin23lem11  8197  fincssdom  8203  fin23lem26  8205  isf32lem9  8241  ac6num  8359  gchdomtri  8504  gchpwdom  8549  winainflem  8568  tskuni  8658  gruima  8677  gruf  8686  grudomon  8692  elnpi  8865  distrlem4pr  8903  prlem934  8910  addcan  9250  addcan2  9251  ltmul1a  9859  ledivmulOLD  9884  ledivmul2OLD  9888  suprleub  9972  supmul1  9973  infmrgelb  9988  suprzcl  10349  uzsupss  10568  xleadd1a  10832  xlesubadd  10842  xmulasslem3  10865  xlemul2a  10868  xadddilem  10873  xadddi2  10876  ixxun  10932  icoshftf1o  11020  lincmb01cmp  11038  iccf1o  11039  ltexp2a  11431  leexp2  11434  ltexp2r  11436  exple1  11439  expnlbnd2  11510  ccatass  11750  ccatopth  11776  s2f1o  11863  limsupgre  12275  addcn2  12387  mulcn2  12389  dvdsadd2b  12892  dvdsmod  12906  oexpneg  12911  gcdass  13045  rplpwr  13056  rppwr  13057  coprmdvds2  13103  rpmulgcd2  13105  qredeq  13106  rpexp  13120  rpdvds  13124  prmdiveq  13175  odzdvds  13181  coprimeprodsq2  13184  pythagtriplem3  13192  pcdvdsb  13242  pcgcd1  13250  qexpz  13270  pockthg  13274  vdwnnlem1  13363  0ram  13388  ramz2  13392  lubss  14548  lubun  14550  clatleglb  14553  clatglbss  14554  mrelatglb  14610  issubmnd  14724  gsumccat  14787  frmdss2  14808  mulgneg  14908  mulgdirlem  14914  submmulg  14925  subgmulg  14958  nmzsubg  14981  ghmmulg  15018  odmodnn0  15178  odnncl  15183  odmod  15184  odmulgid  15190  odmulgeq  15193  odf1o1  15206  odf1o2  15207  odngen  15211  gexdvdsi  15217  pgpfi1  15229  odcau  15238  subgslw  15250  fislw  15259  lsmssv  15277  lsmless1x  15278  lsmless2x  15279  lsmsubm  15287  lsmmod  15307  lsmmod2  15308  efgred  15380  cntzcmn  15459  ghmplusg  15461  odadd1  15463  odadd2  15464  odadd  15465  lsmcomx  15471  gsumconst  15532  rng1eq0  15702  mulgass2  15710  isabvd  15908  lssintcl  16040  0lmhm  16116  lmhmvsca  16121  reslmhm2b  16130  lspfixed  16200  lspsnat  16217  lidldvgen  16326  issubassa  16383  psrplusgpropd  16629  coe1subfv  16659  coe1mul2  16662  xrsdsreclblem  16744  obselocv  16955  riinopn  16981  neiint  17168  topssnei  17188  restntr  17246  iscnp4  17327  cnconst2  17347  cnrest2  17350  cnprest2  17354  cnpdis  17357  cnt0  17410  cnt1  17414  cnhaus  17418  ordthauslem  17447  cncmp  17455  fiuncmp  17467  sscmp  17468  hauscmp  17470  cnconn  17485  uncon  17492  nlly2i  17539  llynlly  17540  nllyidm  17552  ptrescn  17671  xkococnlem  17691  qtoptop2  17731  qtopss  17747  kqfvima  17762  r0cld  17770  ordthmeolem  17833  fbssint  17870  fmf  17977  fmss  17978  elfm  17979  rnelfmlem  17984  rnelfm  17985  fmco  17993  flimss2  18004  flimss1  18005  flimrest  18015  flftg  18028  cnpflf2  18032  cnpflf  18033  flfcnp  18036  supnfcls  18052  fclsss1  18054  fclsss2  18055  fcfnei  18067  fcfelbas  18068  cnpfcfi  18072  subgntr  18136  opnsubg  18137  cldsubg  18140  ghmcnp  18144  utop2nei  18280  neipcfilu  18326  bldisj  18428  blgt0  18429  bl2in  18430  blss2ps  18433  blss2  18434  blssps  18454  blss  18455  xmetresbl  18467  lpbl  18533  blcld  18535  stdbdbl  18547  metcnp3  18570  metcnp2  18572  txmetcnp  18577  blval2  18605  nmoix  18763  nmoeq0  18770  icoopnst  18964  iocopnst  18965  xrhmeo  18971  nmhmcn  19128  cphsqrcl2  19149  cphsqrcl3  19150  cfil3i  19222  caublcls  19261  bcthlem5  19281  cmetcusp1OLD  19305  cmetcusp1  19306  pjth  19340  ovoliunlem2  19399  volun  19439  volsup2  19497  mbfimaopn2  19549  iblconst  19709  itgconst  19710  dvcnp2  19806  dvcn  19807  evlsval2  19941  deg1mul3le  20039  deg1tmle  20040  dvdsq1p  20083  ig1peu  20094  ig1pdvds  20099  coeid3  20159  dgrmulc  20189  efcvx  20365  tanord  20440  logdivlti  20515  logccv  20554  recxpcl  20566  cxpeq  20641  ang180  20656  isosctrlem2  20663  cxp2lim  20815  amgm  20829  muval1  20916  dvdssqf  20921  mumullem2  20963  mumul  20964  bcmono  21061  lgsfcl2  21086  lgsdilem  21106  lgsdirprm  21113  lgsdir  21114  lgsdi  21116  lgsne0  21117  2pthon  21602  gxcom  21857  gxnn0add  21862  zerdivemp1  22022  nvmul0or  22133  ipval2lem2  22200  ipval2lem5  22206  lnomul  22261  shless  22861  shlej1  22862  pjspansn  23079  hoadddi  23306  kbmul  23458  homco2  23480  kbass2  23620  snunioc  24137  eliccelico  24140  elicoelioo  24141  iocinioc2  24142  iocinif  24144  ress0g  24182  xrge0adddir  24215  xrge0npcan  24216  rhmdvdsr  24256  pstmfval  24291  fmcncfil  24317  zrhnm  24353  qqhnm  24374  measvunilem  24566  volfiniune  24586  dya2iocnrect  24631  probun  24677  probinc  24679  cndprob01  24693  pconpi1  24924  cvmsss2  24961  ntrivcvgmul  25230  binomrisefac  25358  dvdspw  25369  br6  25380  br4  25381  frrlem4  25585  brbtwn2  25844  colinearalglem1  25845  colinearalg  25849  axcgrtr  25854  axsegconlem8  25863  axsegconlem9  25864  axsegconlem10  25865  axcontlem8  25910  axcontlem10  25912  cgrcomim  25923  cgrtriv  25936  cgrextend  25942  segconeq  25944  btwntriv2  25946  btwnintr  25953  btwnexch3  25954  btwnouttr2  25956  trisegint  25962  cgrsub  25979  cgrxfr  25989  btwnxfr  25990  lineext  26010  btwnconn1lem13  26033  btwnconn1lem14  26034  btwnconn3  26037  segcon2  26039  brsegle  26042  brsegle2  26043  segletr  26048  segleantisym  26049  seglelin  26050  outsideofeu  26065  lineunray  26081  lineelsb2  26082  areacirc  26297  ivthALT  26338  finlocfin  26379  cocanfo  26419  upixp  26431  ismtyima  26512  rrndstprj2  26540  zerdivemp1x  26571  mzprename  26806  eldioph2lem1  26818  lzunuz  26826  rencldnfi  26882  pellexlem2  26893  infmrgelbi  26941  pellfundglb  26948  pellfund14gap  26950  qirropth  26971  rmxycomplete  26980  congadd  27031  acongeq  27048  jm2.19  27064  jm2.23  27067  jm2.20nn  27068  jm2.27  27079  jm3.1  27091  aomclem6  27134  lnmepi  27160  lmhmfgsplit  27161  lmhmlnmsplit  27162  pwssplit1  27165  pwssplit3  27167  pwssplit4  27168  uvcresum  27219  frlmsslsp  27225  frlmup4  27230  enfixsn  27234  lindff1  27267  f1lindf  27269  lsslindf  27277  islindf4  27285  lbslcic  27288  hbtlem2  27305  hbtlem5  27309  dgraa0p  27331  pmtrfb  27383  psgnunilem4  27397  mhmvlin  27429  hashgcdlem  27493  proot1hash  27496  stoweidlem19  27744  stoweidlem20  27745  stoweidlem22  27747  stoweidlem28  27753  stoweidlem34  27759  stoweidlem44  27769  stoweidlem60  27785  wallispilem3  27792  fzofzim  28136  fzoopth  28139  swrd0swrd  28197  swrdswrdlem  28198  swrdccatin12  28214  bnj517  29256  bnj594  29283  lubunNEW  29771  lsatfixedN  29807  lssat  29814  eqlkr  29897  eqlkr2  29898  lkrlsp  29900  lshpkrlem4  29911  opposet  29980  cvrcon3b  30075  cvrcmp  30081  atlen0  30108  atnle  30115  atlatmstc  30117  cvlatexch3  30136  cvlsupr2  30141  hlsupr2  30184  hlrelat2  30200  cvrexchlem  30216  lnnat  30224  atcvrj2b  30229  atle  30233  atexchcvrN  30237  atbtwn  30243  athgt  30253  3dimlem3  30258  3dim1  30264  1cvratlt  30271  1cvrjat  30272  ps-1  30274  ps-2  30275  3atlem3  30282  3atlem5  30284  3atlem7  30286  llni  30305  llni2  30309  atcvrlln2  30316  llnexatN  30318  llncmp  30319  2llnmat  30321  2at0mat0  30322  lplni  30329  lplnnle2at  30338  2atnelpln  30341  lplnllnneN  30353  llncvrlpln2  30354  2lplnmN  30356  2llnmj  30357  lplncmp  30359  lplnexatN  30360  lplnexllnN  30361  2llnm3N  30366  lvoli  30372  lvoli3  30374  islvol2aN  30389  4atlem0a  30390  4atlem3  30393  4atlem3a  30394  4atlem4a  30396  4atlem4b  30397  4atlem4c  30398  4atlem4d  30399  4atlem10b  30402  4atlem11  30406  4atlem12  30409  lplncvrlvol2  30412  lvolcmp  30414  2lplnmj  30419  islinei  30537  pmapglbx  30566  linepmap  30572  lneq2at  30575  lnjatN  30577  lncvrat  30579  lncmp  30580  2llnma3r  30585  elpaddatriN  30600  elpaddat  30601  paddcom  30610  paddss1  30614  paddss2  30615  paddss12  30616  paddasslem6  30622  paddasslem7  30623  paddasslem8  30624  paddasslem9  30625  paddasslem15  30631  pmodlem2  30644  pmodl42N  30648  pmapjoin  30649  llnmod1i2  30657  2polcon4bN  30715  polcon2bN  30717  poml4N  30750  poml6N  30752  osumcllem1N  30753  osumcllem2N  30754  osumcllem11N  30763  osumclN  30764  pmapojoinN  30765  pexmidlem2N  30768  pexmidlem3N  30769  pexmidlem4N  30770  pexmidlem6N  30772  pexmidlem7N  30773  pl42lem2N  30777  pl42lem3N  30778  pl42lem4N  30779  pl42N  30780  lhpexle2lem  30806  lhpexle3lem  30808  lhpexle3  30809  lhpmcvr3  30822  lhp2at0nle  30832  lhprelat3N  30837  4atex  30873  4atex2  30874  lauteq  30892  lautco  30894  ltrncoidN  30925  ltrneq2  30945  ltrnnidn  30971  ltrnideq  30972  trlnid  30976  ltrnatlw  30980  trlnle  30983  trlval3  30984  trlval4  30985  cdlemc  30994  cdlemd5  30999  cdlemd9  31003  ltrneq3  31005  cdleme0moN  31022  cdleme20  31121  cdleme21j  31133  cdleme21  31134  cdleme27cl  31163  cdlemefrs29bpre0  31193  cdlemefs27cl  31210  cdlemefs32sn1aw  31211  cdleme43fsv1snlem  31217  cdleme32d  31241  cdleme32f  31243  cdleme32le  31244  cdleme35h2  31254  cdleme38n  31261  cdleme40m  31264  cdleme41snaw  31273  cdleme42ke  31282  cdleme17d3  31293  cdleme48fvg  31297  cdlemeg46fvcl  31303  cdlemeg46fgN  31331  cdleme48gfv1  31333  cdleme48fgv  31335  cdleme50trn3  31350  trlord  31366  ltrniotavalbN  31381  cdlemb3  31403  cdlemg6c  31417  cdlemg6  31420  cdlemg7N  31423  cdlemg8c  31426  cdlemg8  31428  cdlemg11a  31434  cdlemg11b  31439  cdlemg12e  31444  cdlemg15a  31452  cdlemg15  31453  cdlemg16  31454  cdlemg16z  31456  cdlemg16zz  31457  cdlemg17dN  31460  cdlemg18a  31475  cdlemg20  31482  cdlemg22  31484  cdlemg24  31485  cdlemg37  31486  cdlemg31d  31497  cdlemg29  31502  cdlemg33b  31504  cdlemg33  31508  cdlemg38  31512  cdlemg39  31513  cdlemg40  31514  trlco  31524  trlcone  31525  cdlemg42  31526  cdlemg44b  31529  ltrncom  31535  trljco  31537  tendococl  31569  tendoplcl  31578  tendoplcom  31579  cdlemj2  31619  cdlemj3  31620  tendoid0  31622  tendoconid  31626  tendotr  31627  cdlemk25-3  31701  cdlemk26b-3  31702  cdlemk34  31707  cdlemk36  31710  cdlemk38  31712  cdlemkid4  31731  cdlemk35s-id  31735  cdlemk39s-id  31737  cdlemk19x  31740  cdlemk53  31754  cdlemk55  31758  cdlemk55u  31763  cdlemk39u  31765  cdlemk19u  31767  cdlemk56  31768  tendoex  31772  cdleml3N  31775  cdleml5N  31777  tendospcanN  31821  cdlemm10N  31916  cdlemn11pre  32008  dihord2pre  32023  dihvalcqpre  32033  dihopelvalcpre  32046  dihord6apre  32054  dihord5b  32057  dihord5apre  32060  dihord  32062  dihmeetlem1N  32088  dihglblem5apreN  32089  dihglblem3N  32093  dihmeetlem2N  32097  dihglbcpreN  32098  dihmeetbN  32101  dihmeetlem4preN  32104  dihmeetlem5  32106  dihmeetlem7N  32108  dihmeetlem10N  32114  dihmeetlem11N  32115  dihmeetlem12N  32116  dihmeetlem13N  32117  dihmeetlem15N  32119  dihmeetlem16N  32120  dihmeetlem17N  32121  dihmeetlem18N  32122  dihmeetlem19N  32123  dihmeetALTN  32125  dih1dimatlem0  32126  dihlspsnssN  32130  dihlspsnat  32131  mapdh8ad  32577  hdmap14lem14  32682  hgmapvvlem3  32726
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator