MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpan Structured version   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  3262  sbnfc2  3309  ssdifss  3478  uneqdifeq  3716  elssuni  4043  riinrab  4166  difexg  4351  rabexg  4353  abssexg  4384  snexALT  4385  copsexg  4442  oteqex  4449  trsuc  4666  oneli  4689  on0eqel  4699  unexb  4709  opeluu  4715  rabxfr  4745  reuhyp  4751  onminesb  4778  onminsb  4779  onintrab  4781  onnminsb  4784  limuni3  4832  tfindsg2  4841  dfom2  4847  brrelexi  4918  brrelex2i  4919  xpss2  4985  opabid2  5004  eliunxp  5012  releldmi  5106  relelrni  5107  dmexg  5130  rnexg  5131  elres  5181  resexg  5185  relbrcnvg  5243  brcodir  5253  soirri  5260  sotri  5261  sotri2  5263  sotri3  5264  soirriOLD  5265  sotriOLD  5266  dfrel2  5321  coi1  5385  fco  5600  fssres  5610  fabexg  5624  fvco4i  5801  fvopab3g  5802  mpteqb  5819  fvimacnv  5845  ffvelrni  5869  fvconst2  5947  resfunexgALT  5958  mptexg  5965  oprabid  6105  ovprc  6108  ndmov  6231  caovcl  6241  caovass  6247  caovdi  6266  ofexg  6309  ot1stg  6361  ot2ndg  6362  ot3rdg  6363  fo1stres  6370  fo2ndres  6371  elopabi  6412  mpt2exxg  6422  frxp  6456  mpt2ndm0  6473  brtpos  6488  rntpos  6492  iunonOLD  6601  smores  6614  tfrlem9a  6647  tfrlem14  6652  tz7.44-2  6665  tz7.44-3  6666  rdgsucmptf  6686  rdglim2  6690  frsucmpt  6695  tz7.48lem  6698  tz7.48-2  6699  tz7.48-1  6700  tz7.49  6702  seqomlem4  6710  abianfplem  6715  abianfp  6716  ordgt0ge1  6741  oe0m  6762  oesuclem  6769  oacl  6779  omcl  6780  oecl  6781  oa0r  6782  om0r  6783  om1r  6786  oe1m  6788  oawordeulem  6797  oaass  6804  odi  6822  omass  6823  oneo  6824  oen0  6829  oewordi  6834  oewordri  6835  oeoalem  6839  oeoa  6840  oeoelem  6841  oeoe  6842  nna0r  6852  nnm0r  6853  nn2m  6893  nnneo  6894  nneob  6895  ecdmn0  6947  ecelqsi  6960  ectocl  6972  brecop2  6998  mapsnf1o  7103  bren  7117  f1oen  7128  ssdomg  7153  map1  7185  snfi  7187  fiprc  7188  xpsnen2g  7201  xpdom1  7207  pwdom  7259  pwen  7280  limenpsi  7282  limensuci  7283  infensuc  7285  php  7291  fineqv  7324  en1eqsn  7338  findcard3  7350  nnsdomg  7366  xpfi  7378  ixpfi2  7405  dffi2  7428  marypha1lem  7438  wofib  7514  card2on  7522  card2inf  7523  wdompwdom  7546  en2lp  7571  inf0  7576  nnsdom  7608  cantnfval2  7624  cantnfle  7626  cantnflt  7627  cnfcom  7657  zfregs  7668  r1sdom  7700  r1val1  7712  tz9.12lem3  7715  rankwflemb  7719  rankf  7720  rankr1ag  7728  rankr1bg  7729  rankr1clem  7746  rankr1c  7747  rankonidlem  7754  unbndrank  7768  rankr1b  7790  rankval4  7793  rankxplim3  7805  rankxpsuc  7806  tcrank  7808  scott0  7810  isnum3  7841  ficardom  7848  cardsdomel  7861  harsdom  7882  cardmin2  7885  infxpenlem  7895  infxpidm2  7898  finacn  7931  alephon  7950  alephcard  7951  alephordi  7955  alephsucdom  7960  alephgeom  7963  alephdom2  7968  alephprc  7980  alephfp  7989  ackbij2lem1  8099  ackbij1lem3  8102  ackbij1lem18  8117  cfeq0  8136  cfsuc  8137  cff1  8138  cflim2  8143  cofsmo  8149  fin4en1  8189  fin23lem21  8219  fin23lem28  8220  fin23lem30  8222  isf32lem5  8237  fin1a2lem4  8283  fin1a2lem13  8292  axcc2lem  8316  axdc3lem4  8333  axdc4lem  8335  zorn2lem4  8379  zorn2lem5  8380  zorn  8387  ttukeylem3  8391  axdclem  8399  brdom7disj  8409  brdom6disj  8410  cardmin  8439  infinf  8441  konigthlem  8443  alephreg  8457  pwcfsdom  8458  fpwwe2lem8  8512  fpwwe  8521  pwcdandom  8542  gchpwdom  8549  winafp  8572  wunr1om  8594  wunfi  8596  tskr1om  8642  tskr1om2  8643  inar1  8650  tskcard  8656  gruina  8693  grur1a  8694  grur1  8695  grothac  8705  indpi  8784  nqereu  8806  nqerrel  8809  ltsonq  8846  prub  8871  genpnnp  8882  distrlem4pr  8903  ltapr  8922  addcanpr  8923  suplem2pr  8930  0nsr  8954  ltsosr  8969  sqgt0sr  8981  mappsrpr  8983  map2psrpr  8985  supsrlem  8986  axpre-lttri  9040  mulid2  9089  0re  9091  axmulgt0  9150  lttri2  9157  lttri3  9158  lttri4  9159  ltnr  9168  ltnsym2  9173  ne0gt0  9178  eqlei  9183  eqlei2  9184  muladd11  9236  mul02lem1  9242  cnegex2  9248  0cnALT  9295  negcl  9306  negneg  9351  mulm1  9475  lt0neg2  9535  le0neg2  9537  msqgt0i  9564  recextlem1  9652  recex  9654  recclzi  9739  recne0zi  9740  recidzi  9741  divasszi  9764  divmulzi  9765  divdirzi  9766  rerecclzi  9778  ltp1  9848  lemul1a  9864  recp1lt1  9908  squeeze0  9913  recgt0i  9915  ltmul1i  9929  ltdiv1i  9930  ltmuldivi  9931  ltmul2i  9932  lemul1i  9933  lemul2i  9934  ledivp1i  9936  ltdivp1i  9937  suprubii  9979  suprlubii  9980  suprnubii  9981  suprleubii  9982  riotaneg  9983  nnrecre  10036  nn0addcl  10255  nn0mulcl  10256  recnz  10345  peano5uzi  10358  dfuzi  10360  eluz2b1  10547  uz2m1nn  10550  zq  10580  nnrecq  10597  rpge0  10624  rpreccl  10635  rpneg  10641  mnflt  10722  pnfnlt  10725  mnfle  10729  xrlttri2  10735  xrlttri3  10736  xrltne  10753  ngtmnft  10755  qbtwnxr  10786  qsqueeze  10787  xlt0neg2  10806  xle0neg2  10808  xaddpnf2  10813  xaddmnf2  10815  xaddid2  10826  xmullem  10843  xmul02  10847  xmulpnf2  10854  xmulmnf2  10856  xmulid2  10859  xmulm1  10860  xmulge0  10863  xmulasslem  10864  xrsupsslem  10885  xrinfmsslem  10886  elioomnf  10999  1fv  11120  4fvwrd4  11121  fzshftral  11134  uzrdglem  11297  uzrdgfni  11298  uzrdgsuci  11300  fzennn  11307  fsequb  11314  fseqsupcl  11316  nn0ennn  11318  axdc4uzlem  11321  0exp  11415  sqgt0i  11468  sqlecan  11487  subsq2  11489  crreczi  11504  bernneq  11505  bernneq3  11507  expnbnd  11508  nn0opthlem2  11562  faclbnd  11581  faclbnd2  11582  faclbnd3  11583  faclbnd4lem1  11584  faclbnd4lem3  11586  faclbnd4lem4  11587  hashginv  11622  hashfz1  11630  hashpw  11699  hashf1lem2  11705  wrdexg  11739  ccatlid  11748  s1cl  11755  s1fv  11760  s111  11762  s1co  11802  reim  11914  imcl  11916  crim  11920  rennim  12044  cnpart  12045  resqrex  12056  sqrgt0  12064  absor  12105  absimle  12114  caubnd  12162  sqrthi  12174  sqrcli  12175  sqrgt0i  12176  sqrmsqi  12177  sqrsqi  12178  sqsqri  12179  sqrge0i  12180  absidi  12181  absnidi  12182  lo1o1  12326  serclim0  12371  fz1f1o  12504  fsum2d  12555  fsumcnv  12557  fsumabs  12580  fsumrlim  12590  fsumo1  12591  binom11  12611  harmonic  12638  mertenslem2  12662  efzval  12703  eftlub  12710  efsep  12711  ef4p  12714  efgt1  12717  eflt  12718  sinf  12725  cosf  12726  efi4p  12738  sinneg  12747  cosneg  12748  efival  12753  efmival  12754  sinhval  12755  coshval  12756  cos01gt0  12792  sin02gt0  12793  absefib  12799  efieq1re  12800  demoivre  12801  demoivreALT  12802  rpnnen2lem9  12822  0dvds  12870  dvdslelem  12894  odd2np1lem  12907  odd2np1  12908  divalglem0  12913  divalglem6  12918  divalglem9  12921  bits0e  12941  bits0o  12942  bitsfzolem  12946  bitsinv1  12954  bitsf1  12958  sadid2  12981  sadasslem  12982  sadeq  12984  bitsuz  12986  gcdcllem3  13013  gcd0id  13023  gcdid0  13024  1gcd  13037  bezoutlem1  13038  bezoutlem3  13040  isprm3  13088  odzdvds  13181  opoe  13185  omoe  13186  opeo  13187  omeo  13188  pythagtriplem12  13200  pythagtriplem13  13201  pythagtriplem14  13202  pythagtriplem16  13204  pc2dvds  13252  pockthi  13275  unbenlem  13276  1arith2  13296  vdwlem10  13358  vdwlem13  13361  prmlem1a  13429  isstruct2  13478  strle1  13560  0rest  13657  topnid  13663  pwselbasb  13710  xpscg  13783  xpsc0  13785  xpsc1  13786  brssc  14014  isfull  14107  isfth  14111  homahom  14194  homadm  14195  homacd  14196  homadmcd  14197  drsdirfi  14395  pwsdiagmhm  14768  gsumws1  14785  mulg0  14895  mulg1  14897  mulg2  14899  odlem2  15177  gexlem2  15216  efgrelexlema  15381  efgredeu  15384  dprdsubg  15582  ablfac1eulem  15630  rngidval  15666  dvdsr  15751  lbsex  16237  sralem  16249  psrbag  16431  subrgply1  16627  ply1sclid  16679  ply1coe  16684  cnfldinv  16732  gzrngunit  16764  zlpir  16771  prmirredlem  16773  prmirred  16775  zlmassa  16805  tpsexOLD  16984  tgval  17020  tgss3  17051  indistopon  17065  iscldtop  17159  restsn  17234  pnfnei  17284  bwth  17473  2ndcdisj  17519  iskgen2  17580  fbasfip  17900  fclsrest  18056  ptcmplem2  18084  divstgpopn  18149  divstgplem  18150  trust  18259  restutop  18267  restutopopn  18268  ustuqtop3  18273  utop2nei  18280  fmucnd  18322  stdbdmetval  18544  metustfbasOLD  18595  metustfbas  18596  nmogelb  18750  iocmnfcld  18803  cnbl0  18808  cnblcld  18809  blssioo  18826  resubmet  18833  xrtgioo  18837  reconn  18859  rectbntr0  18863  fsumcn  18900  cncfmet  18938  iirev  18954  iihalf1  18956  iihalf2  18958  xrhmeo  18971  icccvx  18975  cnheibor  18980  phtpyid  19014  pcorevlem  19051  iscmet3lem2  19245  iscmet3  19246  ovolsslem  19380  ovolunlem1a  19392  ovolicc2lem4  19416  nulmbl2  19431  iundisj2  19443  dyadf  19483  dyadovol  19485  subopnmbl  19496  ismbfcn  19523  mbfimaopnlem  19547  itg1addlem4  19591  itg2leub  19626  itg2seq  19634  itgfsum  19718  limcresi  19772  cnlimc  19775  dvnff  19809  dvnadd  19815  dvcj  19836  dvmptfsum  19859  c1liplem1  19880  evl1rhm  19949  pf1mpf  19972  tdeglem4  19983  mdegldg  19989  mdegcl  19992  deg1z  20010  plypf1  20131  0dgr  20164  coemulc  20173  plyremlem  20221  qaa  20240  aannenlem2  20246  aaliou3lem2  20260  aaliou3lem8  20262  aaliou3lem6  20265  ulmval  20296  abelth  20357  reeff1olem  20362  reeff1o  20363  ef2kpi  20386  sinperlem  20388  sin2kpi  20391  cos2kpi  20392  sinhalfpip  20400  sinhalfpim  20401  coshalfpip  20402  coshalfpim  20403  sincosq1sgn  20406  sinq12gt0  20415  sincos6thpi  20423  sinkpi  20427  sineq0  20429  resinf1o  20438  tanord1  20439  tanord  20440  eflog  20474  logef  20476  dvrelog  20528  dvlog  20542  efopn  20549  0cxp  20557  cxpge0  20574  cxplea  20587  root1id  20638  isosctrlem1  20662  isosctrlem2  20663  asinlem  20708  asinlem2  20709  asinf  20712  atandm2  20717  asinneg  20726  efiasin  20728  sinasin  20729  asinbnd  20739  asinrebnd  20741  cosasin  20744  atans2  20771  leibpilem1  20780  leibpilem2  20781  leibpisum  20783  log2cnv  20784  log2tlbnd  20785  log2ublem2  20787  ftalem3  20857  ftalem5  20859  basellem1  20863  basellem2  20864  basellem4  20866  basellem5  20867  basellem8  20870  0sgm  20927  ppieq0  20959  chpeq0  20992  chteq0  20993  chtublem  20995  chtub  20996  pcbcctr  21060  bcp1ctr  21063  bclbnd  21064  bposlem1  21068  bposlem2  21069  m1lgs  21146  chebbnd1lem1  21163  chtppilim  21169  pntrsumbnd2  21261  pntibnd  21287  qrngneg  21317  ostth  21333  umgrafi  21357  usgraedg4  21406  cusgrarn  21468  wlkntrllem3  21561  constr1trl  21588  1pthon  21591  3v3e3cycl1  21631  constr3trllem2  21638  constr3pthlem1  21642  constr3pthlem3  21644  4cycl4v4e  21653  4cycl4dv4e  21655  0conngra  21661  iseupa  21687  grpo2grp  21822  issubgoi  21898  addinv  21940  ablomul  21943  mulid  21944  rngoi  21968  drngoi  21995  rngoablo2  22010  rngoidmlem  22011  vafval  22082  smfval  22084  0vfval  22085  nvop2  22087  vsfval  22114  nvop  22166  cnnvdemo  22171  imsmetlem  22182  lnocoi  22258  nmoubi  22273  nmoub3i  22274  nmlno0lem  22294  nmlnogt0  22298  nmblolbii  22300  blocnilem  22305  phop  22319  ipasslem1  22332  ipasslem2  22333  ipasslem4  22335  ipasslem5  22336  ipasslem9  22339  ipasslem11  22341  siilem1  22352  siii  22354  ipblnfi  22357  ip2eqi  22358  ubthlem1  22372  ubthlem2  22373  ubthlem3  22374  minvecolem3  22378  htthlem  22420  axhvass-zf  22487  axhvaddid-zf  22489  axhvmulid-zf  22491  axhvmulass-zf  22492  axhvdistr1-zf  22493  axhvdistr2-zf  22494  axhvmul0-zf  22495  axhis2-zf  22498  axhis3-zf  22499  axhcompl-zf  22501  hvsubf  22518  hvsubcl  22520  hv2neg  22530  hvaddsubval  22535  hvsub4  22539  hvaddsub12  22540  hvpncan  22541  hvaddsubass  22543  hvsubass  22546  hvsubdistr1  22551  hvaddeq0  22571  hvsubcan  22576  his2sub  22594  hi01  22598  normneg  22646  hilablo  22662  hilnormi  22665  bcsiALT  22681  hhssnv  22764  occllem  22805  spanval  22835  spancl  22838  shslubi  22887  ococin  22910  pjcli  22919  pjhcli  22920  h1de2ctlem  23057  spanunsni  23081  cm0  23111  chscllem2  23140  spansncvi  23154  pjjsi  23202  pjrni  23204  pjdsi  23214  pjoi0i  23220  mayete3i  23230  mayete3iOLD  23231  ho0val  23253  hocoi  23267  homulid2  23303  hosubneg  23310  hosubdi  23311  honegsubdi  23313  honegsubdi2  23314  hosub4  23316  hoaddsubass  23318  hosubsub4  23321  eigrei  23337  eigposi  23339  eigorthi  23340  nmopsetretHIL  23367  adj1  23436  lnopeq0i  23510  hmopd  23525  nmbdoplbi  23527  nmcexi  23529  nmcoplbi  23531  lnopconi  23537  nmbdfnlbi  23552  nmcfnlbi  23555  lnfnconi  23558  nmopadjlei  23591  nmopcoi  23598  branmfn  23608  cnvbraval  23613  cnvbracl  23614  cnvbrabra  23615  bracnvbra  23616  leoppos  23629  opsqrlem1  23643  pjnmopi  23651  hmopidmpji  23655  pjnormssi  23671  pjtoi  23682  pjadj3  23691  pjclem4a  23701  pj3lem1  23709  pj3si  23710  strlem4  23757  strlem5  23758  hstrlem4  23765  hstrlem5  23766  jplem1  23771  mdslle1i  23820  mdslle2i  23821  mdslj1i  23822  mdslj2i  23823  mdsl1i  23824  mdsl2i  23825  mdslmd1lem1  23828  mdslmd1lem2  23829  mdslmd2i  23833  csmdsymi  23837  mdexchi  23838  elat2  23843  shatomici  23861  shatomistici  23864  chrelati  23867  chrelat2i  23868  cvbr4i  23870  cvexchlem  23871  atomli  23885  atordi  23887  chirredlem4  23896  atcvat3i  23899  atcvat4i  23900  atabsi  23904  mdsymlem1  23906  mdsymlem3  23908  mdsymlem5  23910  sumdmdlem2  23922  cdj1i  23936  abrexdomjm  23988  disjdifprg  24017  disjxpin  24028  iundisj2f  24030  xppreima  24059  xgepnf  24116  xrofsup  24126  iundisj2fi  24153  tpr2rico  24310  mndpluscn  24312  qqhcn  24375  indf1ofs  24423  esumeq2  24433  esumpcvgval  24468  hasheuni  24475  esumcvg  24476  prsiga  24514  measbasedom  24556  measvuni  24568  cntmeas  24580  volmeas  24587  dya2ub  24620  dya2icoseg  24627  ballotlemfc0  24750  zetacvg  24799  eflgam  24829  subfacval2  24873  subfaclim  24874  erdszelem5  24881  erdszelem8  24884  cvmsss2  24961  cvmlift2lem1  24989  cvmlift2lem12  25001  cvmliftphtlem  25004  ghomgrpilem2  25097  zmodid2  25114  relexp1  25131  mulge0b  25191  prodfclim1  25221  prodsn  25286  fprod2d  25305  fprodcnv  25307  fallrisefac  25341  risefacfac  25351  binomrisefac  25358  dfpo2  25378  opelco3  25403  dfon2lem3  25412  dfon2lem7  25416  rdgprc  25422  elpredim  25451  soseq  25529  wfrlem10  25547  wfrlem16  25553  wlimeq2  25572  sltirr  25625  slttr  25626  slttri  25628  slttrieq2  25629  bdayelon  25635  nocvxminlem  25645  nocvxmin  25646  nobndlem1  25647  nobndlem2  25648  nofulllem5  25661  fnimage  25774  imageval  25775  fullfunfv  25792  altopeq2  25809  brbtwn2  25844  colinearalglem4  25848  ax5seglem1  25867  ax5seglem2  25868  ax5seglem5  25872  axbtwnid  25878  axlowdimlem9  25889  axlowdimlem12  25892  axlowdimlem16  25896  axlowdimlem17  25897  axcontlem2  25904  axcontlem7  25909  bpoly0  26096  bpoly1  26097  bpoly2  26103  bpoly3  26104  bpoly4  26105  fsumcube  26106  limsucncmpi  26195  onint1  26199  mblfinlem1  26243  mblfinlem2  26244  mblfinlem4  26246  ismblfin  26247  ovoliunnfl  26248  voliunnfl  26250  mbfresfi  26253  cnambfre  26255  itg2addnclem  26256  itg2addnc  26259  ftc1anclem5  26284  ftc2nc  26289  opnrebl2  26324  comppfsc  26387  abrexdom  26432  incsequz2  26453  isbnd2  26492  totbndbnd  26498  prdsbnd  26502  cntotbnd  26505  heiborlem3  26522  heiborlem6  26525  heibor  26530  repwsmet  26543  rrntotbnd  26545  isdrngo1  26572  iscrngo2  26608  prtlem400  26719  ismrc  26755  mzpresrename  26807  mzpcompact2lem  26808  eluzrabdioph  26866  rencldnfilem  26881  reglogltb  26954  reglogleb  26955  rmspecnonsq  26970  rmspecfund  26972  rmspecpos  26979  rmxypos  27012  jm3.1  27091  ttac  27107  pw2f1ocnv  27108  aomclem6  27134  pwssplit4  27168  frlmpws  27195  frlmlss  27196  frlmpwsfi  27197  frlmsca  27198  frlmbas  27200  frlmbasf  27205  uvcff  27217  frlmpwfi  27239  numinfctb  27245  isnumbasgrplem3  27247  islinds2  27260  islindf4  27285  hausgraph  27508  dvconstbi  27528  rabexgf  27671  aovprc  28028  aovrcl  28029  otthg  28064  oprabv  28085  2leaddle2  28092  wrdlenge2n0  28176  prmgt1  28223  lswrdcshw  28266  wlkop  28297  el2wlksotot  28349  usgfiregdegfi  28361  sinh-conventional  28482  dpfrac1  28515  sgnp  28520  elogb  28532  eel000cT  28806  eelT00  28808  eel00000  28834  eel00cT  28882  bnj519  29103  bnj157  29230  bnj546  29267  cdleme31fv  31187
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