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

Theorem mpan 651
Description: An inference based on modus ponens. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)
Hypotheses
Ref Expression
mpan.1  |-  ph
mpan.2  |-  ( (
ph  /\  ps )  ->  ch )
Assertion
Ref Expression
mpan  |-  ( ps 
->  ch )

Proof of Theorem mpan
StepHypRef Expression
1 mpan.1 . . 3  |-  ph
21a1i 10 . 2  |-  ( ps 
->  ph )
3 mpan.2 . 2  |-  ( (
ph  /\  ps )  ->  ch )
42, 3mpancom 650 1  |-  ( ps 
->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  mp2an  653  mpanl12  663  mp3an1  1264  mp3an12  1267  mp3an13  1268  csbex  3092  sbnfc2  3141  ssdifss  3307  uneqdifeq  3542  elssuni  3855  riinrab  3977  difexg  4162  rabexg  4164  abssexg  4195  snexALT  4196  copsexg  4252  oteqex  4259  trsuc  4476  oneli  4500  on0eqel  4510  unexb  4520  opeluu  4526  rabxfr  4556  reuhyp  4562  onminesb  4589  onminsb  4590  onintrab  4592  onnminsb  4595  limuni3  4643  tfindsg2  4652  dfom2  4658  brrelexi  4729  brrelex2i  4730  xpss2  4796  opabid2  4815  eliunxp  4823  releldmi  4915  relelrni  4916  dmexg  4939  rnexg  4940  elres  4990  resexg  4994  relbrcnvg  5052  brcodir  5062  soirri  5069  sotri  5070  sotri2  5072  sotri3  5073  soirriOLD  5074  sotriOLD  5075  dfrel2  5124  coi1  5188  fco  5398  fssres  5408  fabexg  5422  fvco4i  5597  fvopab3g  5598  mpteqb  5614  fvimacnv  5640  ffvelrni  5664  fvconst2  5729  resfunexgALT  5738  mptexg  5745  oprabid  5882  ovprc  5885  ndmov  6004  caovcl  6014  caovass  6020  caovdi  6039  ofexg  6082  ot1stg  6134  ot2ndg  6135  ot3rdg  6136  fo1stres  6143  fo2ndres  6144  elopabi  6185  mpt2exxg  6195  frxp  6225  brtpos  6243  rntpos  6247  iunonOLD  6356  smores  6369  tfrlem9a  6402  tfrlem14  6407  tz7.44-2  6420  tz7.44-3  6421  rdgsucmptf  6441  rdglim2  6445  frsucmpt  6450  tz7.48lem  6453  tz7.48-2  6454  tz7.48-1  6455  tz7.49  6457  seqomlem4  6465  abianfplem  6470  abianfp  6471  ordgt0ge1  6496  oe0m  6517  oesuclem  6524  oacl  6534  omcl  6535  oecl  6536  oa0r  6537  om0r  6538  om1r  6541  oe1m  6543  oawordeulem  6552  oaass  6559  odi  6577  omass  6578  oneo  6579  oen0  6584  oewordi  6589  oewordri  6590  oeoalem  6594  oeoa  6595  oeoelem  6596  oeoe  6597  nna0r  6607  nnm0r  6608  nn2m  6648  nnneo  6649  nneob  6650  ecdmn0  6702  ecelqsi  6715  ectocl  6727  brecop2  6752  mapsnf1o  6857  bren  6871  f1oen  6882  ssdomg  6907  map1  6939  snfi  6941  fiprc  6942  xpsnen2g  6955  xpdom1  6961  pwdom  7013  pwen  7034  limenpsi  7036  limensuci  7037  infensuc  7039  php  7045  fineqv  7078  en1eqsn  7088  findcard3  7100  nnsdomg  7116  xpfi  7128  ixpfi2  7154  dffi2  7176  marypha1lem  7186  wofib  7260  card2on  7268  card2inf  7269  wdompwdom  7292  en2lp  7317  inf0  7322  nnsdom  7354  cantnfval2  7370  cantnfle  7372  cantnflt  7373  cnfcom  7403  zfregs  7414  r1sdom  7446  r1val1  7458  tz9.12lem3  7461  rankwflemb  7465  rankf  7466  rankr1ag  7474  rankr1bg  7475  rankr1clem  7492  rankr1c  7493  rankonidlem  7500  unbndrank  7514  rankr1b  7536  rankval4  7539  rankxplim3  7551  rankxpsuc  7552  tcrank  7554  scott0  7556  isnum3  7587  ficardom  7594  cardsdomel  7607  harsdom  7628  cardmin2  7631  infxpenlem  7641  infxpidm2  7644  finacn  7677  alephon  7696  alephcard  7697  alephordi  7701  alephsucdom  7706  alephgeom  7709  alephdom2  7714  alephprc  7726  alephfp  7735  ackbij2lem1  7845  ackbij1lem3  7848  ackbij1lem18  7863  cfeq0  7882  cfsuc  7883  cff1  7884  cflim2  7889  cofsmo  7895  fin4en1  7935  fin23lem21  7965  fin23lem28  7966  fin23lem30  7968  isf32lem5  7983  fin1a2lem4  8029  fin1a2lem13  8038  axcc2lem  8062  axdc3lem4  8079  axdc4lem  8081  zorn2lem4  8126  zorn2lem5  8127  zorn  8134  ttukeylem3  8138  axdclem  8146  brdom7disj  8156  brdom6disj  8157  cardmin  8186  infinf  8188  konigthlem  8190  alephreg  8204  pwcfsdom  8205  fpwwe2lem8  8259  fpwwe  8268  pwcdandom  8289  gchpwdom  8296  winafp  8319  wunr1om  8341  wunfi  8343  tskr1om  8389  tskr1om2  8390  inar1  8397  tskcard  8403  gruina  8440  grur1a  8441  grur1  8442  grothac  8452  indpi  8531  nqereu  8553  nqerrel  8556  ltsonq  8593  prub  8618  genpnnp  8629  distrlem4pr  8650  ltapr  8669  addcanpr  8670  suplem2pr  8677  0nsr  8701  ltsosr  8716  sqgt0sr  8728  mappsrpr  8730  map2psrpr  8732  supsrlem  8733  axpre-lttri  8787  mulid2  8836  0re  8838  axmulgt0  8897  lttri2  8904  lttri3  8905  lttri4  8906  ltnr  8915  ltnsym2  8920  ne0gt0  8925  muladd11  8982  mul02lem1  8988  cnegex2  8994  0cnALT  9041  negcl  9052  negneg  9097  mulm1  9221  lt0neg2  9281  le0neg2  9283  msqgt0i  9310  recextlem1  9398  recex  9400  recclzi  9485  recne0zi  9486  recidzi  9487  divasszi  9510  divmulzi  9511  divdirzi  9512  rerecclzi  9524  ltp1  9594  lemul1a  9610  recp1lt1  9654  squeeze0  9659  recgt0i  9661  ltmul1i  9675  ltdiv1i  9676  ltmuldivi  9677  ltmul2i  9678  lemul1i  9679  lemul2i  9680  ledivp1i  9682  ltdivp1i  9683  suprubii  9725  suprlubii  9726  suprnubii  9727  suprleubii  9728  riotaneg  9729  nnrecre  9782  nn0addcl  9999  nn0mulcl  10000  recnz  10087  peano5uzi  10100  dfuzi  10102  eluz2b1  10289  uz2m1nn  10292  zq  10322  nnrecq  10339  rpge0  10366  rpreccl  10377  rpneg  10383  mnflt  10464  pnfnlt  10467  mnfle  10470  xrlttri2  10476  xrlttri3  10477  xrltne  10494  ngtmnft  10496  qbtwnxr  10527  qsqueeze  10528  xlt0neg2  10547  xle0neg2  10549  xaddpnf2  10554  xaddmnf2  10556  xaddid2  10567  xmullem  10584  xmul02  10588  xmulpnf2  10595  xmulmnf2  10597  xmulid2  10600  xmulm1  10601  xmulge0  10604  xmulasslem  10605  xrsupsslem  10625  xrinfmsslem  10626  elioomnf  10738  fzshftral  10869  uzrdglem  11020  uzrdgfni  11021  uzrdgsuci  11023  fzennn  11030  fsequb  11037  fseqsupcl  11039  nn0ennn  11041  axdc4uzlem  11044  0exp  11137  sqgt0i  11190  sqlecan  11209  subsq2  11211  crreczi  11226  bernneq  11227  bernneq3  11229  expnbnd  11230  nn0opthlem2  11284  faclbnd  11303  faclbnd2  11304  faclbnd3  11305  faclbnd4lem1  11306  faclbnd4lem3  11308  faclbnd4lem4  11309  hashginv  11341  hashfz1  11345  hashpw  11388  hashf1lem2  11394  wrdexg  11425  ccatlid  11434  s1cl  11441  s1fv  11446  s111  11448  s1co  11488  reim  11594  imcl  11596  crim  11600  rennim  11724  cnpart  11725  resqrex  11736  sqrgt0  11744  absor  11785  absimle  11794  caubnd  11842  sqrthi  11854  sqrcli  11855  sqrgt0i  11856  sqrmsqi  11857  sqrsqi  11858  sqsqri  11859  sqrge0i  11860  absidi  11861  absnidi  11862  lo1o1  12006  serclim0  12051  fz1f1o  12183  fsum2d  12234  fsumcnv  12236  fsumabs  12259  fsumrlim  12269  fsumo1  12270  binom11  12290  harmonic  12317  mertenslem2  12341  efzval  12382  eftlub  12389  efsep  12390  ef4p  12393  efgt1  12396  eflt  12397  sinf  12404  cosf  12405  efi4p  12417  sinneg  12426  cosneg  12427  efival  12432  efmival  12433  sinhval  12434  coshval  12435  cos01gt0  12471  sin02gt0  12472  absefib  12478  efieq1re  12479  demoivre  12480  demoivreALT  12481  rpnnen2lem9  12501  0dvds  12549  dvdslelem  12573  odd2np1lem  12586  odd2np1  12587  divalglem0  12592  divalglem6  12597  divalglem9  12600  bits0e  12620  bitsfzolem  12625  bitsinv1  12633  bitsf1  12637  sadid2  12660  sadasslem  12661  sadeq  12663  bitsuz  12665  gcdcllem3  12692  gcd0id  12702  gcdid0  12703  1gcd  12716  bezoutlem1  12717  bezoutlem3  12719  isprm3  12767  odzdvds  12860  opoe  12864  omoe  12865  opeo  12866  omeo  12867  pythagtriplem12  12879  pythagtriplem13  12880  pythagtriplem14  12881  pythagtriplem16  12883  pc2dvds  12931  pockthi  12954  unbenlem  12955  1arith2  12975  vdwlem10  13037  vdwlem13  13040  prmlem1a  13108  isstruct2  13157  strle1  13239  0rest  13334  topnid  13340  pwselbasb  13387  xpscg  13460  xpsc0  13462  xpsc1  13463  brssc  13691  isfunc  13738  isfull  13784  isfth  13788  homahom  13871  homadm  13872  homacd  13873  homadmcd  13874  drsdirfi  14072  pwsdiagmhm  14445  gsumws1  14462  mulg0  14572  mulg1  14574  mulg2  14576  odlem2  14854  gexlem2  14893  efgrelexlema  15058  efgredeu  15061  dprdsubg  15259  ablfac1eulem  15307  rngidval  15343  dvdsr  15428  lbsex  15918  sralem  15930  psrbag  16112  subrgply1  16311  ply1sclid  16363  ply1coe  16368  cnfldinv  16405  gzrngunit  16437  zlpir  16444  prmirredlem  16446  prmirred  16448  zlmassa  16478  tpsexOLD  16657  tgval  16693  tgss3  16724  indistopon  16738  iscldtop  16832  restsn  16901  pnfnei  16950  2ndcdisj  17182  iskgen2  17243  fbasfip  17563  fclsrest  17719  ptcmplem2  17747  divstgpopn  17802  divstgplem  17803  stdbdmetval  18060  nmogelb  18225  iocmnfcld  18278  cnbl0  18283  cnblcld  18284  blssioo  18301  resubmet  18308  xrtgioo  18312  reconn  18333  rectbntr0  18337  fsumcn  18374  cncfmet  18412  iirev  18427  iihalf1  18429  iihalf2  18431  xrhmeo  18444  icccvx  18448  cnheibor  18453  phtpyid  18487  pcorevlem  18524  iscmet3lem2  18718  iscmet3  18719  ovolsslem  18843  ovolunlem1a  18855  ovolicc2lem4  18879  nulmbl2  18894  iundisj2  18906  dyadf  18946  dyadovol  18948  subopnmbl  18959  ismbfcn  18986  mbfimaopnlem  19010  itg1addlem4  19054  itg2leub  19089  itg2seq  19097  itgfsum  19181  limcresi  19235  cnlimc  19238  dvnff  19272  dvnadd  19278  dvcj  19299  dvmptfsum  19322  c1liplem1  19343  evl1rhm  19412  pf1mpf  19435  tdeglem4  19446  mdegldg  19452  mdegcl  19455  deg1z  19473  plypf1  19594  0dgr  19627  coemulc  19636  plyremlem  19684  qaa  19703  aannenlem2  19709  aaliou3lem2  19723  aaliou3lem8  19725  aaliou3lem6  19728  ulmval  19759  abelth  19817  reeff1olem  19822  reeff1o  19823  ef2kpi  19846  sinperlem  19848  sin2kpi  19851  cos2kpi  19852  sinhalfpip  19860  sinhalfpim  19861  coshalfpip  19862  coshalfpim  19863  sincosq1sgn  19866  sinq12gt0  19875  sincos6thpi  19883  sinkpi  19887  sineq0  19889  resinf1o  19898  tanord1  19899  tanord  19900  eflog  19933  logef  19935  dvrelog  19984  dvlog  19998  efopn  20005  0cxp  20013  cxpge0  20030  cxplea  20043  root1id  20094  isosctrlem1  20118  isosctrlem2  20119  asinlem  20164  asinlem2  20165  asinf  20168  atandm2  20173  asinneg  20182  efiasin  20184  sinasin  20185  asinbnd  20195  asinrebnd  20197  cosasin  20200  atans2  20227  leibpilem1  20236  leibpilem2  20237  leibpisum  20239  log2cnv  20240  log2tlbnd  20241  log2ublem2  20243  ftalem3  20312  ftalem5  20314  basellem1  20318  basellem2  20319  basellem4  20321  basellem5  20322  basellem8  20325  0sgm  20382  ppieq0  20414  chpeq0  20447  chteq0  20448  chtublem  20450  chtub  20451  pcbcctr  20515  bcp1ctr  20518  bclbnd  20519  bposlem1  20523  bposlem2  20524  m1lgs  20601  chebbnd1lem1  20618  chtppilim  20624  pntrsumbnd2  20716  pntibnd  20742  qrngneg  20772  ostth  20788  grpo2grp  20901  issubgoi  20977  addinv  21019  ablomul  21022  mulid  21023  rngoi  21047  drngoi  21074  rngoablo2  21089  rngoidmlem  21090  vafval  21159  smfval  21161  0vfval  21162  nvop2  21164  vsfval  21191  nvop  21243  cnnvdemo  21248  imsmetlem  21259  lnocoi  21335  nmoubi  21350  nmoub3i  21351  nmlno0lem  21371  nmlnogt0  21375  nmblolbii  21377  blocnilem  21382  phop  21396  ipasslem1  21409  ipasslem2  21410  ipasslem4  21412  ipasslem5  21413  ipasslem9  21416  ipasslem11  21418  siilem1  21429  siii  21431  ipblnfi  21434  ip2eqi  21435  ubthlem1  21449  ubthlem2  21450  ubthlem3  21451  minvecolem3  21455  htthlem  21497  axhvass-zf  21564  axhvaddid-zf  21566  axhvmulid-zf  21568  axhvmulass-zf  21569  axhvdistr1-zf  21570  axhvdistr2-zf  21571  axhvmul0-zf  21572  axhis2-zf  21575  axhis3-zf  21576  axhcompl-zf  21578  hvsubf  21595  hvsubcl  21597  hv2neg  21607  hvaddsubval  21612  hvsub4  21616  hvaddsub12  21617  hvpncan  21618  hvaddsubass  21620  hvsubass  21623  hvsubdistr1  21628  hvaddeq0  21648  hvsubcan  21653  his2sub  21671  hi01  21675  normneg  21723  hilablo  21739  hilnormi  21742  bcsiALT  21758  hhssnv  21841  occllem  21882  spanval  21912  spancl  21915  shslubi  21964  ococin  21987  pjcli  21996  pjhcli  21997  h1de2ctlem  22134  spanunsni  22158  cm0  22188  chscllem2  22217  spansncvi  22231  pjjsi  22279  pjrni  22281  pjdsi  22291  pjoi0i  22297  mayete3i  22307  mayete3iOLD  22308  ho0val  22330  hocoi  22344  homulid2  22380  hosubneg  22387  hosubdi  22388  honegsubdi  22390  honegsubdi2  22391  hosub4  22393  hoaddsubass  22395  hosubsub4  22398  eigrei  22414  eigposi  22416  eigorthi  22417  nmopsetretHIL  22444  adj1  22513  lnopeq0i  22587  hmopd  22602  nmbdoplbi  22604  nmcexi  22606  nmcoplbi  22608  lnopconi  22614  nmbdfnlbi  22629  nmcfnlbi  22632  lnfnconi  22635  nmopadjlei  22668  nmopcoi  22675  branmfn  22685  cnvbraval  22690  cnvbracl  22691  cnvbrabra  22692  bracnvbra  22693  leoppos  22706  opsqrlem1  22720  pjnmopi  22728  hmopidmpji  22732  pjnormssi  22748  pjtoi  22759  pjadj3  22768  pjclem4a  22778  pj3lem1  22786  pj3si  22787  strlem4  22834  strlem5  22835  hstrlem4  22842  hstrlem5  22843  jplem1  22848  mdslle1i  22897  mdslle2i  22898  mdslj1i  22899  mdslj2i  22900  mdsl1i  22901  mdsl2i  22902  mdslmd1lem1  22905  mdslmd1lem2  22906  mdslmd2i  22910  csmdsymi  22914  mdexchi  22915  elat2  22920  shatomici  22938  shatomistici  22941  chrelati  22944  chrelat2i  22945  cvbr4i  22947  cvexchlem  22948  atomli  22962  atordi  22964  chirredlem4  22973  atcvat3i  22976  atcvat4i  22977  atabsi  22981  mdsymlem1  22983  mdsymlem3  22985  mdsymlem5  22987  sumdmdlem2  22999  cdj1i  23013  ballotlem2  23047  ballotlemfc0  23051  ballotlem4  23057  xgtpnf  23114  abrexdomjm  23165  xppreima  23211  xrofsup  23255  tpr2rico  23296  mndpluscn  23299  mptct  23345  mptctf  23348  disjdifprg  23352  iundisj2fi  23364  iundisj2f  23366  esumeq2  23418  esumpcvgval  23446  hasheuni  23453  esumcvg  23454  dmvlsiga  23490  prsiga  23492  difelsiga  23494  measbasedom  23532  measvuni  23542  cntmeas  23553  dya2ub  23575  dya2iocseg  23579  indf1ofs  23609  zetacvg  23689  subfacval2  23718  subfaclim  23719  erdszelem5  23726  erdszelem8  23729  cvmsss2  23805  cvmlift2lem1  23833  cvmlift2lem12  23845  cvmliftphtlem  23848  umgrafi  23874  iseupa  23881  ghomgrpilem2  23993  zmodid2  24010  relexp1  24027  mulge0b  24086  dfpo2  24112  dfon2lem3  24141  dfon2lem7  24145  rdgprc  24151  elpredim  24176  soseq  24254  wfrlem10  24265  wfrlem16  24271  sltirr  24324  slttr  24325  slttri  24327  slttrieq2  24328  bdayelon  24334  nocvxminlem  24344  nocvxmin  24345  nobndlem1  24346  nobndlem2  24347  nofulllem5  24360  fnimage  24468  imageval  24469  funpartfv  24483  fullfunfv  24485  altopeq2  24498  brbtwn2  24533  colinearalglem4  24537  ax5seglem1  24556  ax5seglem2  24557  ax5seglem5  24561  axbtwnid  24567  axlowdimlem9  24578  axlowdimlem12  24581  axlowdimlem16  24585  axlowdimlem17  24586  axcontlem2  24593  axcontlem7  24598  bpoly0  24785  bpoly1  24786  bpoly2  24792  bpoly3  24793  bpoly4  24794  fsumcube  24795  limsucncmpi  24884  onint1  24888  copsexgb  24966  prl  25167  preoref22  25229  int2pre  25237  ranncnt  25283  fprodp1  25323  seqzp2  25355  sallnei  25529  hmeogrpi  25536  qusp  25542  efilcp  25552  islimrs4  25582  bwt2  25592  altretop  25600  mslb1  25607  hdrmp  25706  domval  25723  codval  25724  idval  25725  cmpval  25726  dedalg  25743  catded  25764  valtar  25883  pwtsm  25889  subtsm  25890  subtareqbe  25891  1iskle  25989  pfsubkl  26047  pgapspf  26052  sgplpte21d1  26139  sgplpte21d2  26140  opnrebl2  26236  comppfsc  26307  abrexdom  26405  incsequz2  26459  isbnd2  26507  totbndbnd  26513  prdsbnd  26517  cntotbnd  26520  heiborlem3  26537  heiborlem6  26540  heibor  26545  repwsmet  26558  rrntotbnd  26560  isdrngo1  26587  iscrngo2  26623  prtlem400  26738  ismrc  26776  mzpresrename  26828  mzpcompact2lem  26829  eluzrabdioph  26887  rencldnfilem  26903  reglogltb  26976  reglogleb  26977  rmspecnonsq  26992  rmspecfund  26994  rmspecpos  27001  rmxypos  27034  jm3.1  27113  ttac  27129  pw2f1ocnv  27130  aomclem6  27156  pwssplit4  27191  frlmpws  27218  frlmlss  27219  frlmpwsfi  27220  frlmsca  27221  frlmbas  27223  frlmbasf  27228  uvcff  27240  frlmpwfi  27262  numinfctb  27268  isnumbasgrplem3  27270  islinds2  27283  islindf4  27308  hausgraph  27531  dvconstbi  27551  rabexgf  27695  aovprc  28048  aovrcl  28049  mpt2ndm0  28078  sinh-conventional  28209  dpfrac1  28242  sgnp  28247  eel000cT  28478  eelT00  28480  eel001  28487  eel00cT  28545  bnj519  28764  bnj157  28891  bnj546  28928  cdleme31fv  30579
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 177  df-an 360
  Copyright terms: Public domain W3C validator