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

Theorem mpan2 654
Description: An inference based on modus ponens. (Contributed by NM, 16-Sep-1993.) (Proof shortened by Wolf Lammen, 19-Nov-2012.)
Hypotheses
Ref Expression
mpan2.1  |-  ps
mpan2.2  |-  ( (
ph  /\  ps )  ->  ch )
Assertion
Ref Expression
mpan2  |-  ( ph  ->  ch )

Proof of Theorem mpan2
StepHypRef Expression
1 mpan2.1 . . 3  |-  ps
21a1i 11 . 2  |-  ( ph  ->  ps )
3 mpan2.2 . 2  |-  ( (
ph  /\  ps )  ->  ch )
42, 3mpdan 651 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  mpanr12  668  mp3an23  1272  equs4OLD  1999  eueq2  3109  sbcgf  3225  csbconstgf  3265  sbcnestg  3301  csbnestg  3302  csbnest1g  3304  mpteq1  4290  iinexg  4361  nnullss  4426  ord0eln0  4636  eusv2nf  4722  reusv2lem5  4729  eldifpw  4756  ordeleqon  4770  ordsson  4771  ssnlim  4864  xpss1  4985  xpiindi  5011  reldm0  5088  elrnmpt1s  5119  resdm  5185  resid  5198  eliniseg  5234  trinxp  5260  inimasn  5290  ssrnres  5310  cnveq0  5328  coi2  5387  relrelss  5394  funcnvres  5523  funimaex  5532  fnresin1  5560  fnresin2  5561  fresin  5613  dffv3  5725  ssimaex  5789  dmfco  5798  fvmpt  5807  fvmptnf  5823  fvimacnvALT  5850  dff3  5883  fsn  5907  fsn2  5909  elabrex  5986  f1elima  6010  fliftel1  6033  f1owe  6074  2ndconst  6437  curry1  6439  tposfun  6496  tpostpos2  6501  sorpssuni  6532  sorpssint  6533  riotasv  6598  tfrlem10  6649  tfrlem12  6651  tfr3  6661  seqomlem1  6708  seqomlem2  6709  seqomlem4  6711  abianfplem  6716  ondif2  6747  oa0  6761  om0  6762  oa1suc  6776  om1  6786  oe1  6788  oe1m  6789  omass  6824  oeoalem  6840  oeoelem  6842  nnmsucr  6869  nnm1  6892  nnm2  6893  ecelqsg  6960  xpider  6976  qsel  6984  map0e  7052  fvdiagfn  7059  ixpsnf1o  7103  map1  7186  xp1en  7195  sbthlem7  7224  domunsn  7258  xpmapenlem  7275  infensuc  7286  infi  7333  finresfin  7335  diffi  7340  dif1enOLD  7341  dif1en  7342  unblem1  7360  unblem2  7361  unblem3  7362  unblem4  7363  isfinite2  7366  infn0  7370  unfilem1  7372  unfilem2  7373  unfir  7376  fofinf1o  7388  cnvfi  7391  pwfilem  7402  mptfi  7407  finsschain  7414  marypha2  7445  inf0  7577  trcl  7665  r1rankidb  7731  snwf  7736  unwf  7737  uniwf  7746  rankval3b  7753  rankr1a  7763  rankxplim3  7806  scott0  7811  card1  7856  pm54.43  7888  infxpenc2  7904  dfac8clem  7914  alephsuc2  7962  alephle  7970  cardaleph  7971  dfacacn  8022  dfac13  8023  dfac12lem2  8025  cdaval  8051  uncdadom  8052  cdaun  8053  cdacomen  8062  cdaassen  8063  cdadom1  8067  cdainf  8073  pwcda1  8075  ackbij1lem18  8118  cflem  8127  cflecard  8134  cfeq0  8137  cfslb  8147  cfsmolem  8151  cfcoflem  8153  cfidm  8156  isfin4-3  8196  fin23lem12  8212  fin23lem16  8216  fin23lem28  8221  fin23lem38  8230  fin23lem41  8233  fin1a2lem7  8287  fin1a2lem12  8292  fin1a2lem13  8293  hsmexlem8  8305  axcc2lem  8317  axcc3  8319  domtriomlem  8323  axdc3lem2  8332  axdc3lem4  8334  axdc4lem  8336  axcclem  8338  ac6num  8360  ttukeylem4  8393  ttukeylem7  8396  ttukey2g  8397  axdclem  8400  brdom3  8407  brdom5  8408  cardeq0  8428  unsnen  8429  konigthlem  8444  pwcfsdom  8459  canthp1lem1  8528  wunex2  8614  wuncval2  8623  eltsk2g  8627  intgru  8690  ingru  8691  grutsk  8698  axgroth6  8704  mulidpi  8764  nlt1pi  8784  indpi  8785  pinq  8805  mulidnq  8841  1idpr  8907  prlem934  8911  0idsr  8973  1idsr  8974  00sr  8975  negexsr  8978  recexsrlem  8979  sqgt0sr  8982  ax1rid  9037  axcnre  9040  ne0gt0  9179  peano2cn  9239  peano2re  9240  00id  9242  mul02lem2  9244  mul01  9246  subid  9322  subid1  9323  negid  9349  negeq0  9356  peano2rem  9368  lt0neg1  9535  le0neg1  9537  div2neg  9738  recgt0ii  9917  divgt0i2i  9927  ledivp1i  9937  ltdivp1i  9938  peano5nni  10004  peano2nn  10013  nnge1  10027  times2  10101  addltmul  10204  nn0p1nn  10260  peano2nn0  10261  elnnnn0  10264  nn0lele2xi  10273  peano2z  10319  peano2zm  10321  nn0lt10b  10337  suprzcl  10350  zeo  10356  uzindOLD  10365  uzwo  10540  uzwoOLD  10541  uzwo2  10542  infmssuzle  10559  infmssuzcl  10560  rpnnen1lem1  10601  rpnnen1lem3  10603  rpnnen1lem5  10605  rphalfcl  10637  ltpnf  10722  nltmnf  10727  pnfge  10728  nltpnft  10755  qsqueeze  10788  xlt0neg1  10806  xle0neg1  10808  xaddpnf1  10813  xaddmnf1  10815  xaddid1  10826  xsubge0  10841  xmul01  10847  xmulneg1  10849  xmulpnf1  10854  xmulid1  10859  supxrbnd  10908  supxrgtmnf  10909  supxrre1  10910  supxrre2  10911  elioopnf  10999  elicopnf  11001  iccshftri  11032  iccshftli  11034  iccdili  11036  icccntri  11038  fzprval  11107  fzofzp1  11190  fzostep1  11198  injresinj  11201  flge0nn0  11226  flge1nn  11227  btwnzge0  11231  modfrac  11262  om2uzsuci  11289  axdc4uzlem  11322  ser1const  11380  exp0  11387  exp1  11388  expn1  11392  expubnd  11441  sqval  11442  sqeq0  11447  resqcl  11450  zsqcl  11453  binom21  11498  expnbnd  11509  nn0opthlem2  11563  facnn2  11576  faclbnd4lem3  11587  faclbnd5  11590  bcnn  11604  bcn2  11611  bcn2p1  11617  hasheq0  11645  hashsng  11648  hashdif  11679  hash2pr  11688  hash2prde  11689  hashxplem  11697  hashf1lem2  11706  iswrd  11730  wrdval  11731  ccatval2  11747  ccatrid  11750  s111  11763  shftfib  11888  reim0  11924  imval2  11957  cjne0  11969  abssq  12112  max0add  12116  abs2dif  12137  rddif  12145  absrdbnd  12146  rexuz3  12153  rlimdm  12346  isershft  12458  isercolllem2  12460  isercoll  12462  fsum  12515  fsumadd  12533  bcxmas  12616  infcvgaux2i  12638  efi4p  12739  resin4p  12740  recos4p  12741  sinbnd  12782  cosbnd  12783  znnenlem  12812  rpnnen2lem8  12822  rpnnen2  12826  cnso  12847  dvdsmul2  12873  dvdslelem  12895  odd2np1lem  12908  divalglem0  12914  divalglem1  12915  divalglem4  12917  divalglem5  12918  divalglem8  12921  bits0  12941  bitsp1o  12946  bitsf1  12959  sadadd2lem2  12963  gcd1  13033  gcdmultiple  13051  isprm3  13089  phiprm  13167  pc0  13229  pcdvdstr  13250  vdwlem2  13351  vdwlem6  13355  vdwlem8  13357  hashbc0  13374  setsval  13494  setsres  13496  ressinbas  13526  ressress  13527  elrestr  13657  pwssnf1o  13721  xpsfrnel  13789  ismred2  13829  submre  13831  mreacs  13884  oppchomfval  13941  brssc  14015  isssc  14021  yonedalem4c  14375  isprs  14388  lubid  14440  oduleval  14559  oduclatb  14572  gsumval2a  14783  mulg1  14898  mulgnegnn  14901  isghm  15007  cntrnsg  15141  oppgplusfval  15145  efgrelexlemb  15383  frgp0  15393  frgpmhm  15398  vrgpf  15401  cygctb  15502  dprd0  15590  dprd2da  15601  mgpplusg  15653  opprmulfval  15731  subrgint  15891  lsp0  16086  sralem  16250  zcyg  16773  mulgrhm2  16789  zlmsca  16803  chrnzr  16812  ocvz  16906  cssincl  16916  css0  16917  css1  16918  0opn  16978  topopn  16980  basdif0  17019  tgval  17021  unitg  17033  tgdif0  17058  isopn2  17097  0cld  17103  ntropn  17114  ntrval2  17116  ntrdif  17117  clsdif  17118  cmclsopn  17127  cmntrcld  17128  clstop  17134  ntrtop  17135  cls0  17145  ntr0  17146  mretopd  17157  neips  17178  neiptopnei  17197  maxlp  17212  isperf2  17217  rest0  17234  iocpnfordt  17280  icomnfordt  17281  mnfnei  17286  bwth  17474  1stckgen  17587  ptbasfi  17614  pthaus  17671  imasnopn  17723  imasncld  17724  imasncls  17725  fbssfi  17870  isfil2  17889  ssfg  17905  filcon  17916  fbasrn  17917  filufint  17953  imaelfm  17984  fmfnfmlem4  17990  fclsfnflim  18060  alexsubALTlem3  18081  alexsubALTlem4  18082  ustfilxp  18243  ustuqtop1  18272  ustuqtop2  18273  ustuqtop3  18274  ustuqtop4  18275  utopsnneiplem  18278  utopsnnei  18280  utop2nei  18281  cfiluweak  18326  neipcfilu  18327  xmetres  18395  metres  18396  mopnex  18550  prdsms  18562  blval2  18606  metucnOLD  18619  metucn  18620  tngds  18690  nmoge0  18756  cnfldnm  18814  tgioo  18828  xrtgioo  18838  xrsmopn  18844  negcncf  18949  phtpy01  19011  pco0  19040  tchtopn  19185  tchnmfval  19187  caussi  19251  minveclem3b  19330  ovolfioo  19365  ovolficc  19366  ovolfsf  19369  ovolctb  19387  ovolctb2  19389  ovolfiniun  19398  ovoliun2  19403  ovolshftlem1  19406  ovolscalem1  19410  ovolicopnf  19421  iunmbl2  19452  uniioombllem2  19476  opnmblALT  19496  ismbf  19523  mbfinf  19558  0plef  19565  itg1climres  19607  itg2cnlem1  19654  iblitg  19661  ibl0  19679  itgcn  19735  cnlimc  19776  dvfre  19838  dvnfre  19839  dveflem  19864  dvef  19865  dvlipcn  19879  lhop2  19900  itgsubstlem  19933  evl1rhm  19950  ply1rem  20087  coefv0  20167  plyrecj  20198  vieta1lem2  20229  aannenlem1  20246  aaliou2b  20259  ulmval  20297  ulmpm  20300  ulmdvlem1  20317  mtest  20321  efcn  20360  sin2pim  20394  cos2pim  20395  sinmpi  20396  cosmpi  20397  sinppi  20398  cosppi  20399  efimpi  20400  sincosq1lem  20406  sincosq2sgn  20408  sincosq3sgn  20409  sincosq4sgn  20410  sinq12gt0  20416  sinq34lt0t  20418  sincosq1eq  20421  abssinper  20427  efif1o  20449  relogcn  20530  ellogdm  20531  efopn  20550  cxp0  20562  cxp1  20563  cxpsqr  20595  logsqr  20596  atandm3  20719  atanbnd  20767  atancn  20777  leibpi  20783  efrlim  20809  logdifbnd  20833  vmaprm  20901  ppip1le  20945  ppieq0  20960  prmorcht  20962  ppiublem1  20987  ppiub  20989  chpeq0  20993  chtub  20997  fsumvma  20998  pclogsum  21000  chpval2  21003  dchrresb  21044  dchrptlem1  21049  lgs0  21094  lgs2  21098  lgsdir2lem2  21109  lgsdir2lem4  21111  lgsdchrval  21132  lgsdchr  21133  lgseisenlem2  21135  dirith2  21223  selberg2lem  21245  qabvle  21320  qabvexp  21321  ostth  21334  uhgra0  21345  umgra0  21361  umisuhgra  21363  usisuslgra  21388  usgra0  21391  usgraedg4  21407  usgrafisbase  21429  usgrasscusgra  21493  uvtx01vtx  21502  fargshiftlem  21622  usgrcyclnl2  21629  constr3trl  21647  constr3pth  21648  constr3cycl  21649  4cycl4dv  21655  iseupa  21688  ex-po  21744  gx1  21851  addinv  21941  vcoprne  22059  nvnd  22181  ipval2lem3  22202  ipval2  22204  ipval2lem6  22208  4ipval3  22209  ipidsq  22210  dipcj  22214  dip0r  22217  nmlnogt0  22299  blocni  22307  ipasslem2  22334  ipasslem8  22339  ipasslem9  22340  ajval  22364  ubthlem1  22373  hvaddid2  22526  hvsub0  22579  hi02  22600  hlimi  22691  isch2  22727  chlimi  22738  chsupunss  22847  shsupunss  22849  chlejb1i  22979  h1dei  23053  h1de2ci  23059  spanunsni  23082  pjoml2i  23088  pjorthi  23172  mayete3i  23231  mayete3iOLD  23232  hosubid1  23302  nmopge0  23415  nmfnge0  23431  adj1  23437  adjeq  23439  lnop0  23470  lnopmi  23504  nmophmi  23535  cnlnadjlem5  23575  cnlnadjeui  23581  unierri  23608  leoprf2  23631  leopnmid  23642  nmopleid  23643  hstles  23735  hst0  23737  strlem3a  23756  dmdbr2  23807  mdsl1i  23825  mdsl2i  23826  mdsl2bi  23827  cvmdi  23828  mdslmd1lem1  23829  mdslmd1lem2  23830  mdslmd1i  23833  mdslmd2i  23834  csmdsymi  23838  mdexchi  23839  superpos  23858  atomli  23886  atordi  23888  chirredlem1  23894  chirredlem2  23895  atcvat4i  23901  atabsi  23905  mdsymlem1  23907  mdsymlem5  23911  mdsymlem6  23912  sumdmdii  23919  dmdbr5ati  23926  dmdbr6ati  23927  mddmdin0i  23935  cdj3lem2  23939  xppreima  24060  abfmpunirn  24065  abfmpel  24068  xlemnf  24118  xrdifh  24144  clatp0ex  24194  clatp1ex  24195  xrge0neqmnf  24213  metider  24290  rge0scvg  24336  lmxrge0  24338  qqh0  24369  qqh1  24370  zrhre  24386  rnlogblem  24400  logb1  24404  esumcst  24456  esumfzf  24460  esumfsupre  24462  hasheuni  24476  sgon  24508  dmvlsiga  24513  sigainb  24520  measval  24553  ismeas  24554  sxbrsigalem0  24622  rrvsum  24713  ballotlem2  24747  ballotlemfcc  24752  ballotlem4  24757  ptpcon  24921  cvmsss2  24962  cvmlift2lem12  25002  cvmlift2lem13  25003  cvmliftphtlem  25005  cvmliftpht  25006  relin01  25195  bcnm1  25202  fprod  25268  risefac0  25344  fallfac0  25345  risefac1  25350  fallfac1  25351  fprb  25398  opelco3  25404  predreseq  25455  predep  25468  trpred0  25515  wfr3g  25538  wfrlem14  25552  wfrlem15  25553  wlimeq1  25572  frr3g  25582  noxpsgn  25621  funpartfv  25791  imagesset  25799  altopeq1  25809  brbtwn  25839  colinearalglem4  25849  axlowdimlem13  25894  axlowdimlem17  25898  brcolinear2  25993  bpoly2  26104  bpoly3  26105  bpoly4  26106  fsumcube  26107  ontgval  26182  onint1  26200  mblfinlem1  26244  mblfinlem2  26245  mblfinlem3  26246  mblfinlem4  26247  ismblfin  26248  itg2addnclem  26257  itg2addnclem2  26258  itg2addnclem3  26259  itg2addnc  26260  itg2gt0cn  26261  ftc1anclem5  26285  ftc1anclem8  26288  gtinf  26323  cldbnd  26330  ivthALT  26339  refref  26366  refssfne  26375  tailfb  26407  unirep  26415  sdclem2  26447  totbndbnd  26499  heibor1lem  26519  heiborlem7  26527  bfplem1  26532  prnc  26678  fninfp  26736  fndifnfp  26738  fnnfpeq0  26740  ralxpmap  26743  mapfzcons1cl  26775  eldioph3b  26824  eldiophss  26834  0dioph  26838  vdioph  26839  eldioph4b  26873  eldioph4i  26874  rencldnfilem  26882  rmxy1  26986  rmxy0  26987  rmxm1  26998  rmym1  26999  monotoddzzfi  27006  nn0sqcl  27055  aomclem6  27135  pwslnmlem0  27171  pwslnmlem1  27172  isnumbasabl  27249  psgneldm2i  27406  seff  27516  lhe4.4ex1a  27524  fmuldfeqlem1  27689  fmuldfeq  27690  infrglb  27699  climneg  27713  stoweidlem18  27744  stoweidlem19  27745  stoweidlem22  27748  stoweidlem34  27760  stoweidlem40  27766  stoweidlem41  27767  stoweidlem55  27781  stoweidlem59  27785  rlimdmafv  28018  cnm1cn  28089  euhash1  28168  cshw0  28239  usgra2pthspth  28306  usgra2wlkspthlem2  28308  usgra2pthlem1  28311  el2wlkonotlem  28330  usg2wlkonot  28351  usg2wotspth  28352  frgrancvvdeqlemA  28427  eelT0  28888  snssl  28943  sineq0ALT  29050  bnj535  29262  bnj580  29285  bnj907  29337  bnj1253  29387  equs4NEW7  29534  lub0N  29988  glb0N  29992  glbconN  30175  atpointN  30541  polsubN  30705  pol0N  30707  pol1N  30708  2polvalN  30712  2polssN  30713  3polN  30714  pcl0N  30720  2pmaplubN  30724  pnonsingN  30731  polsubclN  30750  cdlemefs32sn1aw  31212  cdleme43fsv1snlem  31218  cdleme41sn3a  31231  cdleme32a  31239  cdleme40m  31265  cdleme40n  31266  cdleme42b  31276  istendo  31558  cdlemk40  31715  cdlemkid  31734  dihvalcqpre  32034
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 179  df-an 362
  Copyright terms: Public domain W3C validator