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

Theorem mpan 652
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 11 . 2  |-  ( ps 
->  ph )
3 mpan.2 . 2  |-  ( (
ph  /\  ps )  ->  ch )
42, 3mpancom 651 1  |-  ( ps 
->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  mp2an  654  mpanl12  664  mp3an1  1266  mp3an12  1269  mp3an13  1270  csbex  3222  sbnfc2  3269  ssdifss  3438  uneqdifeq  3676  elssuni  4003  riinrab  4126  difexg  4311  rabexg  4313  abssexg  4344  snexALT  4345  copsexg  4402  oteqex  4409  trsuc  4625  oneli  4648  on0eqel  4658  unexb  4668  opeluu  4674  rabxfr  4704  reuhyp  4710  onminesb  4737  onminsb  4738  onintrab  4740  onnminsb  4743  limuni3  4791  tfindsg2  4800  dfom2  4806  brrelexi  4877  brrelex2i  4878  xpss2  4944  opabid2  4963  eliunxp  4971  releldmi  5065  relelrni  5066  dmexg  5089  rnexg  5090  elres  5140  resexg  5144  relbrcnvg  5202  brcodir  5212  soirri  5219  sotri  5220  sotri2  5222  sotri3  5223  soirriOLD  5224  sotriOLD  5225  dfrel2  5280  coi1  5344  fco  5559  fssres  5569  fabexg  5583  fvco4i  5760  fvopab3g  5761  mpteqb  5778  fvimacnv  5804  ffvelrni  5828  fvconst2  5906  resfunexgALT  5917  mptexg  5924  oprabid  6064  ovprc  6067  ndmov  6190  caovcl  6200  caovass  6206  caovdi  6225  ofexg  6268  ot1stg  6320  ot2ndg  6321  ot3rdg  6322  fo1stres  6329  fo2ndres  6330  elopabi  6371  mpt2exxg  6381  frxp  6415  mpt2ndm0  6432  brtpos  6447  rntpos  6451  iunonOLD  6560  smores  6573  tfrlem9a  6606  tfrlem14  6611  tz7.44-2  6624  tz7.44-3  6625  rdgsucmptf  6645  rdglim2  6649  frsucmpt  6654  tz7.48lem  6657  tz7.48-2  6658  tz7.48-1  6659  tz7.49  6661  seqomlem4  6669  abianfplem  6674  abianfp  6675  ordgt0ge1  6700  oe0m  6721  oesuclem  6728  oacl  6738  omcl  6739  oecl  6740  oa0r  6741  om0r  6742  om1r  6745  oe1m  6747  oawordeulem  6756  oaass  6763  odi  6781  omass  6782  oneo  6783  oen0  6788  oewordi  6793  oewordri  6794  oeoalem  6798  oeoa  6799  oeoelem  6800  oeoe  6801  nna0r  6811  nnm0r  6812  nn2m  6852  nnneo  6853  nneob  6854  ecdmn0  6906  ecelqsi  6919  ectocl  6931  brecop2  6957  mapsnf1o  7062  bren  7076  f1oen  7087  ssdomg  7112  map1  7144  snfi  7146  fiprc  7147  xpsnen2g  7160  xpdom1  7166  pwdom  7218  pwen  7239  limenpsi  7241  limensuci  7242  infensuc  7244  php  7250  fineqv  7283  en1eqsn  7297  findcard3  7309  nnsdomg  7325  xpfi  7337  ixpfi2  7363  dffi2  7386  marypha1lem  7396  wofib  7470  card2on  7478  card2inf  7479  wdompwdom  7502  en2lp  7527  inf0  7532  nnsdom  7564  cantnfval2  7580  cantnfle  7582  cantnflt  7583  cnfcom  7613  zfregs  7624  r1sdom  7656  r1val1  7668  tz9.12lem3  7671  rankwflemb  7675  rankf  7676  rankr1ag  7684  rankr1bg  7685  rankr1clem  7702  rankr1c  7703  rankonidlem  7710  unbndrank  7724  rankr1b  7746  rankval4  7749  rankxplim3  7761  rankxpsuc  7762  tcrank  7764  scott0  7766  isnum3  7797  ficardom  7804  cardsdomel  7817  harsdom  7838  cardmin2  7841  infxpenlem  7851  infxpidm2  7854  finacn  7887  alephon  7906  alephcard  7907  alephordi  7911  alephsucdom  7916  alephgeom  7919  alephdom2  7924  alephprc  7936  alephfp  7945  ackbij2lem1  8055  ackbij1lem3  8058  ackbij1lem18  8073  cfeq0  8092  cfsuc  8093  cff1  8094  cflim2  8099  cofsmo  8105  fin4en1  8145  fin23lem21  8175  fin23lem28  8176  fin23lem30  8178  isf32lem5  8193  fin1a2lem4  8239  fin1a2lem13  8248  axcc2lem  8272  axdc3lem4  8289  axdc4lem  8291  zorn2lem4  8335  zorn2lem5  8336  zorn  8343  ttukeylem3  8347  axdclem  8355  brdom7disj  8365  brdom6disj  8366  cardmin  8395  infinf  8397  konigthlem  8399  alephreg  8413  pwcfsdom  8414  fpwwe2lem8  8468  fpwwe  8477  pwcdandom  8498  gchpwdom  8505  winafp  8528  wunr1om  8550  wunfi  8552  tskr1om  8598  tskr1om2  8599  inar1  8606  tskcard  8612  gruina  8649  grur1a  8650  grur1  8651  grothac  8661  indpi  8740  nqereu  8762  nqerrel  8765  ltsonq  8802  prub  8827  genpnnp  8838  distrlem4pr  8859  ltapr  8878  addcanpr  8879  suplem2pr  8886  0nsr  8910  ltsosr  8925  sqgt0sr  8937  mappsrpr  8939  map2psrpr  8941  supsrlem  8942  axpre-lttri  8996  mulid2  9045  0re  9047  axmulgt0  9106  lttri2  9113  lttri3  9114  lttri4  9115  ltnr  9124  ltnsym2  9129  ne0gt0  9134  eqlei  9139  eqlei2  9140  muladd11  9192  mul02lem1  9198  cnegex2  9204  0cnALT  9251  negcl  9262  negneg  9307  mulm1  9431  lt0neg2  9491  le0neg2  9493  msqgt0i  9520  recextlem1  9608  recex  9610  recclzi  9695  recne0zi  9696  recidzi  9697  divasszi  9720  divmulzi  9721  divdirzi  9722  rerecclzi  9734  ltp1  9804  lemul1a  9820  recp1lt1  9864  squeeze0  9869  recgt0i  9871  ltmul1i  9885  ltdiv1i  9886  ltmuldivi  9887  ltmul2i  9888  lemul1i  9889  lemul2i  9890  ledivp1i  9892  ltdivp1i  9893  suprubii  9935  suprlubii  9936  suprnubii  9937  suprleubii  9938  riotaneg  9939  nnrecre  9992  nn0addcl  10211  nn0mulcl  10212  recnz  10301  peano5uzi  10314  dfuzi  10316  eluz2b1  10503  uz2m1nn  10506  zq  10536  nnrecq  10553  rpge0  10580  rpreccl  10591  rpneg  10597  mnflt  10678  pnfnlt  10681  mnfle  10685  xrlttri2  10691  xrlttri3  10692  xrltne  10709  ngtmnft  10711  qbtwnxr  10742  qsqueeze  10743  xlt0neg2  10762  xle0neg2  10764  xaddpnf2  10769  xaddmnf2  10771  xaddid2  10782  xmullem  10799  xmul02  10803  xmulpnf2  10810  xmulmnf2  10812  xmulid2  10815  xmulm1  10816  xmulge0  10819  xmulasslem  10820  xrsupsslem  10841  xrinfmsslem  10842  elioomnf  10955  1fv  11075  4fvwrd4  11076  fzshftral  11089  uzrdglem  11252  uzrdgfni  11253  uzrdgsuci  11255  fzennn  11262  fsequb  11269  fseqsupcl  11271  nn0ennn  11273  axdc4uzlem  11276  0exp  11370  sqgt0i  11423  sqlecan  11442  subsq2  11444  crreczi  11459  bernneq  11460  bernneq3  11462  expnbnd  11463  nn0opthlem2  11517  faclbnd  11536  faclbnd2  11537  faclbnd3  11538  faclbnd4lem1  11539  faclbnd4lem3  11541  faclbnd4lem4  11542  hashginv  11577  hashfz1  11585  hashpw  11654  hashf1lem2  11660  wrdexg  11694  ccatlid  11703  s1cl  11710  s1fv  11715  s111  11717  s1co  11757  reim  11869  imcl  11871  crim  11875  rennim  11999  cnpart  12000  resqrex  12011  sqrgt0  12019  absor  12060  absimle  12069  caubnd  12117  sqrthi  12129  sqrcli  12130  sqrgt0i  12131  sqrmsqi  12132  sqrsqi  12133  sqsqri  12134  sqrge0i  12135  absidi  12136  absnidi  12137  lo1o1  12281  serclim0  12326  fz1f1o  12459  fsum2d  12510  fsumcnv  12512  fsumabs  12535  fsumrlim  12545  fsumo1  12546  binom11  12566  harmonic  12593  mertenslem2  12617  efzval  12658  eftlub  12665  efsep  12666  ef4p  12669  efgt1  12672  eflt  12673  sinf  12680  cosf  12681  efi4p  12693  sinneg  12702  cosneg  12703  efival  12708  efmival  12709  sinhval  12710  coshval  12711  cos01gt0  12747  sin02gt0  12748  absefib  12754  efieq1re  12755  demoivre  12756  demoivreALT  12757  rpnnen2lem9  12777  0dvds  12825  dvdslelem  12849  odd2np1lem  12862  odd2np1  12863  divalglem0  12868  divalglem6  12873  divalglem9  12876  bits0e  12896  bits0o  12897  bitsfzolem  12901  bitsinv1  12909  bitsf1  12913  sadid2  12936  sadasslem  12937  sadeq  12939  bitsuz  12941  gcdcllem3  12968  gcd0id  12978  gcdid0  12979  1gcd  12992  bezoutlem1  12993  bezoutlem3  12995  isprm3  13043  odzdvds  13136  opoe  13140  omoe  13141  opeo  13142  omeo  13143  pythagtriplem12  13155  pythagtriplem13  13156  pythagtriplem14  13157  pythagtriplem16  13159  pc2dvds  13207  pockthi  13230  unbenlem  13231  1arith2  13251  vdwlem10  13313  vdwlem13  13316  prmlem1a  13384  isstruct2  13433  strle1  13515  0rest  13612  topnid  13618  pwselbasb  13665  xpscg  13738  xpsc0  13740  xpsc1  13741  brssc  13969  isfull  14062  isfth  14066  homahom  14149  homadm  14150  homacd  14151  homadmcd  14152  drsdirfi  14350  pwsdiagmhm  14723  gsumws1  14740  mulg0  14850  mulg1  14852  mulg2  14854  odlem2  15132  gexlem2  15171  efgrelexlema  15336  efgredeu  15339  dprdsubg  15537  ablfac1eulem  15585  rngidval  15621  dvdsr  15706  lbsex  16192  sralem  16204  psrbag  16386  subrgply1  16582  ply1sclid  16634  ply1coe  16639  cnfldinv  16687  gzrngunit  16719  zlpir  16726  prmirredlem  16728  prmirred  16730  zlmassa  16760  tpsexOLD  16939  tgval  16975  tgss3  17006  indistopon  17020  iscldtop  17114  restsn  17188  pnfnei  17238  2ndcdisj  17472  iskgen2  17533  fbasfip  17853  fclsrest  18009  ptcmplem2  18037  divstgpopn  18102  divstgplem  18103  trust  18212  restutop  18220  restutopopn  18221  ustuqtop3  18226  utop2nei  18233  fmucnd  18275  stdbdmetval  18497  metustfbasOLD  18548  metustfbas  18549  nmogelb  18703  iocmnfcld  18756  cnbl0  18761  cnblcld  18762  blssioo  18779  resubmet  18786  xrtgioo  18790  reconn  18812  rectbntr0  18816  fsumcn  18853  cncfmet  18891  iirev  18907  iihalf1  18909  iihalf2  18911  xrhmeo  18924  icccvx  18928  cnheibor  18933  phtpyid  18967  pcorevlem  19004  iscmet3lem2  19198  iscmet3  19199  ovolsslem  19333  ovolunlem1a  19345  ovolicc2lem4  19369  nulmbl2  19384  iundisj2  19396  dyadf  19436  dyadovol  19438  subopnmbl  19449  ismbfcn  19476  mbfimaopnlem  19500  itg1addlem4  19544  itg2leub  19579  itg2seq  19587  itgfsum  19671  limcresi  19725  cnlimc  19728  dvnff  19762  dvnadd  19768  dvcj  19789  dvmptfsum  19812  c1liplem1  19833  evl1rhm  19902  pf1mpf  19925  tdeglem4  19936  mdegldg  19942  mdegcl  19945  deg1z  19963  plypf1  20084  0dgr  20117  coemulc  20126  plyremlem  20174  qaa  20193  aannenlem2  20199  aaliou3lem2  20213  aaliou3lem8  20215  aaliou3lem6  20218  ulmval  20249  abelth  20310  reeff1olem  20315  reeff1o  20316  ef2kpi  20339  sinperlem  20341  sin2kpi  20344  cos2kpi  20345  sinhalfpip  20353  sinhalfpim  20354  coshalfpip  20355  coshalfpim  20356  sincosq1sgn  20359  sinq12gt0  20368  sincos6thpi  20376  sinkpi  20380  sineq0  20382  resinf1o  20391  tanord1  20392  tanord  20393  eflog  20427  logef  20429  dvrelog  20481  dvlog  20495  efopn  20502  0cxp  20510  cxpge0  20527  cxplea  20540  root1id  20591  isosctrlem1  20615  isosctrlem2  20616  asinlem  20661  asinlem2  20662  asinf  20665  atandm2  20670  asinneg  20679  efiasin  20681  sinasin  20682  asinbnd  20692  asinrebnd  20694  cosasin  20697  atans2  20724  leibpilem1  20733  leibpilem2  20734  leibpisum  20736  log2cnv  20737  log2tlbnd  20738  log2ublem2  20740  ftalem3  20810  ftalem5  20812  basellem1  20816  basellem2  20817  basellem4  20819  basellem5  20820  basellem8  20823  0sgm  20880  ppieq0  20912  chpeq0  20945  chteq0  20946  chtublem  20948  chtub  20949  pcbcctr  21013  bcp1ctr  21016  bclbnd  21017  bposlem1  21021  bposlem2  21022  m1lgs  21099  chebbnd1lem1  21116  chtppilim  21122  pntrsumbnd2  21214  pntibnd  21240  qrngneg  21270  ostth  21286  umgrafi  21310  usgraedg4  21359  cusgrarn  21421  wlkntrllem3  21514  constr1trl  21541  1pthon  21544  3v3e3cycl1  21584  constr3trllem2  21591  constr3pthlem1  21595  constr3pthlem3  21597  4cycl4v4e  21606  4cycl4dv4e  21608  0conngra  21614  iseupa  21640  grpo2grp  21775  issubgoi  21851  addinv  21893  ablomul  21896  mulid  21897  rngoi  21921  drngoi  21948  rngoablo2  21963  rngoidmlem  21964  vafval  22035  smfval  22037  0vfval  22038  nvop2  22040  vsfval  22067  nvop  22119  cnnvdemo  22124  imsmetlem  22135  lnocoi  22211  nmoubi  22226  nmoub3i  22227  nmlno0lem  22247  nmlnogt0  22251  nmblolbii  22253  blocnilem  22258  phop  22272  ipasslem1  22285  ipasslem2  22286  ipasslem4  22288  ipasslem5  22289  ipasslem9  22292  ipasslem11  22294  siilem1  22305  siii  22307  ipblnfi  22310  ip2eqi  22311  ubthlem1  22325  ubthlem2  22326  ubthlem3  22327  minvecolem3  22331  htthlem  22373  axhvass-zf  22440  axhvaddid-zf  22442  axhvmulid-zf  22444  axhvmulass-zf  22445  axhvdistr1-zf  22446  axhvdistr2-zf  22447  axhvmul0-zf  22448  axhis2-zf  22451  axhis3-zf  22452  axhcompl-zf  22454  hvsubf  22471  hvsubcl  22473  hv2neg  22483  hvaddsubval  22488  hvsub4  22492  hvaddsub12  22493  hvpncan  22494  hvaddsubass  22496  hvsubass  22499  hvsubdistr1  22504  hvaddeq0  22524  hvsubcan  22529  his2sub  22547  hi01  22551  normneg  22599  hilablo  22615  hilnormi  22618  bcsiALT  22634  hhssnv  22717  occllem  22758  spanval  22788  spancl  22791  shslubi  22840  ococin  22863  pjcli  22872  pjhcli  22873  h1de2ctlem  23010  spanunsni  23034  cm0  23064  chscllem2  23093  spansncvi  23107  pjjsi  23155  pjrni  23157  pjdsi  23167  pjoi0i  23173  mayete3i  23183  mayete3iOLD  23184  ho0val  23206  hocoi  23220  homulid2  23256  hosubneg  23263  hosubdi  23264  honegsubdi  23266  honegsubdi2  23267  hosub4  23269  hoaddsubass  23271  hosubsub4  23274  eigrei  23290  eigposi  23292  eigorthi  23293  nmopsetretHIL  23320  adj1  23389  lnopeq0i  23463  hmopd  23478  nmbdoplbi  23480  nmcexi  23482  nmcoplbi  23484  lnopconi  23490  nmbdfnlbi  23505  nmcfnlbi  23508  lnfnconi  23511  nmopadjlei  23544  nmopcoi  23551  branmfn  23561  cnvbraval  23566  cnvbracl  23567  cnvbrabra  23568  bracnvbra  23569  leoppos  23582  opsqrlem1  23596  pjnmopi  23604  hmopidmpji  23608  pjnormssi  23624  pjtoi  23635  pjadj3  23644  pjclem4a  23654  pj3lem1  23662  pj3si  23663  strlem4  23710  strlem5  23711  hstrlem4  23718  hstrlem5  23719  jplem1  23724  mdslle1i  23773  mdslle2i  23774  mdslj1i  23775  mdslj2i  23776  mdsl1i  23777  mdsl2i  23778  mdslmd1lem1  23781  mdslmd1lem2  23782  mdslmd2i  23786  csmdsymi  23790  mdexchi  23791  elat2  23796  shatomici  23814  shatomistici  23817  chrelati  23820  chrelat2i  23821  cvbr4i  23823  cvexchlem  23824  atomli  23838  atordi  23840  chirredlem4  23849  atcvat3i  23852  atcvat4i  23853  atabsi  23857  mdsymlem1  23859  mdsymlem3  23861  mdsymlem5  23863  sumdmdlem2  23875  cdj1i  23889  abrexdomjm  23941  disjdifprg  23970  disjxpin  23981  iundisj2f  23983  xppreima  24012  xgepnf  24069  xrofsup  24079  iundisj2fi  24106  tpr2rico  24263  mndpluscn  24265  qqhcn  24328  indf1ofs  24376  esumeq2  24386  esumpcvgval  24421  hasheuni  24428  esumcvg  24429  prsiga  24467  measbasedom  24509  measvuni  24521  cntmeas  24533  volmeas  24540  dya2ub  24573  dya2icoseg  24580  ballotlemfc0  24703  zetacvg  24752  eflgam  24782  subfacval2  24826  subfaclim  24827  erdszelem5  24834  erdszelem8  24837  cvmsss2  24914  cvmlift2lem1  24942  cvmlift2lem12  24954  cvmliftphtlem  24957  ghomgrpilem2  25050  zmodid2  25067  relexp1  25084  mulge0b  25144  prodfclim1  25174  prodsn  25239  fprod2d  25258  fprodcnv  25260  fallrisefac  25293  risefacfac  25301  binomrisefac  25309  dfpo2  25326  dfon2lem3  25355  dfon2lem7  25359  rdgprc  25365  elpredim  25390  soseq  25468  wfrlem10  25479  wfrlem16  25485  sltirr  25538  slttr  25539  slttri  25541  slttrieq2  25542  bdayelon  25548  nocvxminlem  25558  nocvxmin  25559  nobndlem1  25560  nobndlem2  25561  nofulllem5  25574  fnimage  25682  imageval  25683  fullfunfv  25700  altopeq2  25713  brbtwn2  25748  colinearalglem4  25752  ax5seglem1  25771  ax5seglem2  25772  ax5seglem5  25776  axbtwnid  25782  axlowdimlem9  25793  axlowdimlem12  25796  axlowdimlem16  25800  axlowdimlem17  25801  axcontlem2  25808  axcontlem7  25813  bpoly0  26000  bpoly1  26001  bpoly2  26007  bpoly3  26008  bpoly4  26009  fsumcube  26010  limsucncmpi  26099  onint1  26103  mblfinlem  26143  mblfinlem3  26145  ismblfin  26146  ovoliunnfl  26147  voliunnfl  26149  mbfresfi  26152  cnambfre  26154  itg2addnclem  26155  itg2addnc  26158  opnrebl2  26214  comppfsc  26277  abrexdom  26322  incsequz2  26343  isbnd2  26382  totbndbnd  26388  prdsbnd  26392  cntotbnd  26395  heiborlem3  26412  heiborlem6  26415  heibor  26420  repwsmet  26433  rrntotbnd  26435  isdrngo1  26462  iscrngo2  26498  prtlem400  26609  ismrc  26645  mzpresrename  26697  mzpcompact2lem  26698  eluzrabdioph  26756  rencldnfilem  26771  reglogltb  26844  reglogleb  26845  rmspecnonsq  26860  rmspecfund  26862  rmspecpos  26869  rmxypos  26902  jm3.1  26981  ttac  26997  pw2f1ocnv  26998  aomclem6  27024  pwssplit4  27059  frlmpws  27086  frlmlss  27087  frlmpwsfi  27088  frlmsca  27089  frlmbas  27091  frlmbasf  27096  uvcff  27108  frlmpwfi  27130  numinfctb  27136  isnumbasgrplem3  27138  islinds2  27151  islindf4  27176  hausgraph  27399  dvconstbi  27419  rabexgf  27562  aovprc  27919  aovrcl  27920  otthg  27952  el2wlksotot  28079  usgfiregdegfi  28091  sinh-conventional  28196  dpfrac1  28229  sgnp  28234  elogb  28246  eel000cT  28515  eelT00  28517  eel00000  28543  eel00cT  28591  bnj519  28809  bnj157  28936  bnj546  28973  cdleme31fv  30872
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
  Copyright terms: Public domain W3C validator