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  3206  sbnfc2  3253  ssdifss  3422  uneqdifeq  3660  elssuni  3986  riinrab  4108  difexg  4293  rabexg  4295  abssexg  4326  snexALT  4327  copsexg  4384  oteqex  4391  trsuc  4607  oneli  4630  on0eqel  4640  unexb  4650  opeluu  4656  rabxfr  4686  reuhyp  4692  onminesb  4719  onminsb  4720  onintrab  4722  onnminsb  4725  limuni3  4773  tfindsg2  4782  dfom2  4788  brrelexi  4859  brrelex2i  4860  xpss2  4926  opabid2  4945  eliunxp  4953  releldmi  5047  relelrni  5048  dmexg  5071  rnexg  5072  elres  5122  resexg  5126  relbrcnvg  5184  brcodir  5194  soirri  5201  sotri  5202  sotri2  5204  sotri3  5205  soirriOLD  5206  sotriOLD  5207  dfrel2  5262  coi1  5326  fco  5541  fssres  5551  fabexg  5565  fvco4i  5741  fvopab3g  5742  mpteqb  5759  fvimacnv  5785  ffvelrni  5809  fvconst2  5887  resfunexgALT  5898  mptexg  5905  oprabid  6045  ovprc  6048  ndmov  6171  caovcl  6181  caovass  6187  caovdi  6206  ofexg  6249  ot1stg  6301  ot2ndg  6302  ot3rdg  6303  fo1stres  6310  fo2ndres  6311  elopabi  6352  mpt2exxg  6362  frxp  6393  mpt2ndm0  6410  brtpos  6425  rntpos  6429  iunonOLD  6538  smores  6551  tfrlem9a  6584  tfrlem14  6589  tz7.44-2  6602  tz7.44-3  6603  rdgsucmptf  6623  rdglim2  6627  frsucmpt  6632  tz7.48lem  6635  tz7.48-2  6636  tz7.48-1  6637  tz7.49  6639  seqomlem4  6647  abianfplem  6652  abianfp  6653  ordgt0ge1  6678  oe0m  6699  oesuclem  6706  oacl  6716  omcl  6717  oecl  6718  oa0r  6719  om0r  6720  om1r  6723  oe1m  6725  oawordeulem  6734  oaass  6741  odi  6759  omass  6760  oneo  6761  oen0  6766  oewordi  6771  oewordri  6772  oeoalem  6776  oeoa  6777  oeoelem  6778  oeoe  6779  nna0r  6789  nnm0r  6790  nn2m  6830  nnneo  6831  nneob  6832  ecdmn0  6884  ecelqsi  6897  ectocl  6909  brecop2  6935  mapsnf1o  7040  bren  7054  f1oen  7065  ssdomg  7090  map1  7122  snfi  7124  fiprc  7125  xpsnen2g  7138  xpdom1  7144  pwdom  7196  pwen  7217  limenpsi  7219  limensuci  7220  infensuc  7222  php  7228  fineqv  7261  en1eqsn  7275  findcard3  7287  nnsdomg  7303  xpfi  7315  ixpfi2  7341  dffi2  7364  marypha1lem  7374  wofib  7448  card2on  7456  card2inf  7457  wdompwdom  7480  en2lp  7505  inf0  7510  nnsdom  7542  cantnfval2  7558  cantnfle  7560  cantnflt  7561  cnfcom  7591  zfregs  7602  r1sdom  7634  r1val1  7646  tz9.12lem3  7649  rankwflemb  7653  rankf  7654  rankr1ag  7662  rankr1bg  7663  rankr1clem  7680  rankr1c  7681  rankonidlem  7688  unbndrank  7702  rankr1b  7724  rankval4  7727  rankxplim3  7739  rankxpsuc  7740  tcrank  7742  scott0  7744  isnum3  7775  ficardom  7782  cardsdomel  7795  harsdom  7816  cardmin2  7819  infxpenlem  7829  infxpidm2  7832  finacn  7865  alephon  7884  alephcard  7885  alephordi  7889  alephsucdom  7894  alephgeom  7897  alephdom2  7902  alephprc  7914  alephfp  7923  ackbij2lem1  8033  ackbij1lem3  8036  ackbij1lem18  8051  cfeq0  8070  cfsuc  8071  cff1  8072  cflim2  8077  cofsmo  8083  fin4en1  8123  fin23lem21  8153  fin23lem28  8154  fin23lem30  8156  isf32lem5  8171  fin1a2lem4  8217  fin1a2lem13  8226  axcc2lem  8250  axdc3lem4  8267  axdc4lem  8269  zorn2lem4  8313  zorn2lem5  8314  zorn  8321  ttukeylem3  8325  axdclem  8333  brdom7disj  8343  brdom6disj  8344  cardmin  8373  infinf  8375  konigthlem  8377  alephreg  8391  pwcfsdom  8392  fpwwe2lem8  8446  fpwwe  8455  pwcdandom  8476  gchpwdom  8483  winafp  8506  wunr1om  8528  wunfi  8530  tskr1om  8576  tskr1om2  8577  inar1  8584  tskcard  8590  gruina  8627  grur1a  8628  grur1  8629  grothac  8639  indpi  8718  nqereu  8740  nqerrel  8743  ltsonq  8780  prub  8805  genpnnp  8816  distrlem4pr  8837  ltapr  8856  addcanpr  8857  suplem2pr  8864  0nsr  8888  ltsosr  8903  sqgt0sr  8915  mappsrpr  8917  map2psrpr  8919  supsrlem  8920  axpre-lttri  8974  mulid2  9023  0re  9025  axmulgt0  9084  lttri2  9091  lttri3  9092  lttri4  9093  ltnr  9102  ltnsym2  9107  ne0gt0  9112  muladd11  9169  mul02lem1  9175  cnegex2  9181  0cnALT  9228  negcl  9239  negneg  9284  mulm1  9408  lt0neg2  9468  le0neg2  9470  msqgt0i  9497  recextlem1  9585  recex  9587  recclzi  9672  recne0zi  9673  recidzi  9674  divasszi  9697  divmulzi  9698  divdirzi  9699  rerecclzi  9711  ltp1  9781  lemul1a  9797  recp1lt1  9841  squeeze0  9846  recgt0i  9848  ltmul1i  9862  ltdiv1i  9863  ltmuldivi  9864  ltmul2i  9865  lemul1i  9866  lemul2i  9867  ledivp1i  9869  ltdivp1i  9870  suprubii  9912  suprlubii  9913  suprnubii  9914  suprleubii  9915  riotaneg  9916  nnrecre  9969  nn0addcl  10188  nn0mulcl  10189  recnz  10278  peano5uzi  10291  dfuzi  10293  eluz2b1  10480  uz2m1nn  10483  zq  10513  nnrecq  10530  rpge0  10557  rpreccl  10568  rpneg  10574  mnflt  10655  pnfnlt  10658  mnfle  10662  xrlttri2  10668  xrlttri3  10669  xrltne  10686  ngtmnft  10688  qbtwnxr  10719  qsqueeze  10720  xlt0neg2  10739  xle0neg2  10741  xaddpnf2  10746  xaddmnf2  10748  xaddid2  10759  xmullem  10776  xmul02  10780  xmulpnf2  10787  xmulmnf2  10789  xmulid2  10792  xmulm1  10793  xmulge0  10796  xmulasslem  10797  xrsupsslem  10818  xrinfmsslem  10819  elioomnf  10932  1fv  11051  4fvwrd4  11052  fzshftral  11065  uzrdglem  11225  uzrdgfni  11226  uzrdgsuci  11228  fzennn  11235  fsequb  11242  fseqsupcl  11244  nn0ennn  11246  axdc4uzlem  11249  0exp  11343  sqgt0i  11396  sqlecan  11415  subsq2  11417  crreczi  11432  bernneq  11433  bernneq3  11435  expnbnd  11436  nn0opthlem2  11490  faclbnd  11509  faclbnd2  11510  faclbnd3  11511  faclbnd4lem1  11512  faclbnd4lem3  11514  faclbnd4lem4  11515  hashginv  11550  hashfz1  11558  hashpw  11627  hashf1lem2  11633  wrdexg  11667  ccatlid  11676  s1cl  11683  s1fv  11688  s111  11690  s1co  11730  reim  11842  imcl  11844  crim  11848  rennim  11972  cnpart  11973  resqrex  11984  sqrgt0  11992  absor  12033  absimle  12042  caubnd  12090  sqrthi  12102  sqrcli  12103  sqrgt0i  12104  sqrmsqi  12105  sqrsqi  12106  sqsqri  12107  sqrge0i  12108  absidi  12109  absnidi  12110  lo1o1  12254  serclim0  12299  fz1f1o  12432  fsum2d  12483  fsumcnv  12485  fsumabs  12508  fsumrlim  12518  fsumo1  12519  binom11  12539  harmonic  12566  mertenslem2  12590  efzval  12631  eftlub  12638  efsep  12639  ef4p  12642  efgt1  12645  eflt  12646  sinf  12653  cosf  12654  efi4p  12666  sinneg  12675  cosneg  12676  efival  12681  efmival  12682  sinhval  12683  coshval  12684  cos01gt0  12720  sin02gt0  12721  absefib  12727  efieq1re  12728  demoivre  12729  demoivreALT  12730  rpnnen2lem9  12750  0dvds  12798  dvdslelem  12822  odd2np1lem  12835  odd2np1  12836  divalglem0  12841  divalglem6  12846  divalglem9  12849  bits0e  12869  bits0o  12870  bitsfzolem  12874  bitsinv1  12882  bitsf1  12886  sadid2  12909  sadasslem  12910  sadeq  12912  bitsuz  12914  gcdcllem3  12941  gcd0id  12951  gcdid0  12952  1gcd  12965  bezoutlem1  12966  bezoutlem3  12968  isprm3  13016  odzdvds  13109  opoe  13113  omoe  13114  opeo  13115  omeo  13116  pythagtriplem12  13128  pythagtriplem13  13129  pythagtriplem14  13130  pythagtriplem16  13132  pc2dvds  13180  pockthi  13203  unbenlem  13204  1arith2  13224  vdwlem10  13286  vdwlem13  13289  prmlem1a  13357  isstruct2  13406  strle1  13488  0rest  13585  topnid  13591  pwselbasb  13638  xpscg  13711  xpsc0  13713  xpsc1  13714  brssc  13942  isfull  14035  isfth  14039  homahom  14122  homadm  14123  homacd  14124  homadmcd  14125  drsdirfi  14323  pwsdiagmhm  14696  gsumws1  14713  mulg0  14823  mulg1  14825  mulg2  14827  odlem2  15105  gexlem2  15144  efgrelexlema  15309  efgredeu  15312  dprdsubg  15510  ablfac1eulem  15558  rngidval  15594  dvdsr  15679  lbsex  16165  sralem  16177  psrbag  16359  subrgply1  16555  ply1sclid  16607  ply1coe  16612  cnfldinv  16656  gzrngunit  16688  zlpir  16695  prmirredlem  16697  prmirred  16699  zlmassa  16729  tpsexOLD  16908  tgval  16944  tgss3  16975  indistopon  16989  iscldtop  17083  restsn  17157  pnfnei  17207  2ndcdisj  17441  iskgen2  17502  fbasfip  17822  fclsrest  17978  ptcmplem2  18006  divstgpopn  18071  divstgplem  18072  trust  18181  restutop  18189  restutopopn  18190  ustuqtop3  18195  utop2nei  18202  fmucnd  18244  stdbdmetval  18435  metustfbas  18478  nmogelb  18622  iocmnfcld  18675  cnbl0  18680  cnblcld  18681  blssioo  18698  resubmet  18705  xrtgioo  18709  reconn  18731  rectbntr0  18735  fsumcn  18772  cncfmet  18810  iirev  18826  iihalf1  18828  iihalf2  18830  xrhmeo  18843  icccvx  18847  cnheibor  18852  phtpyid  18886  pcorevlem  18923  iscmet3lem2  19117  iscmet3  19118  ovolsslem  19248  ovolunlem1a  19260  ovolicc2lem4  19284  nulmbl2  19299  iundisj2  19311  dyadf  19351  dyadovol  19353  subopnmbl  19364  ismbfcn  19391  mbfimaopnlem  19415  itg1addlem4  19459  itg2leub  19494  itg2seq  19502  itgfsum  19586  limcresi  19640  cnlimc  19643  dvnff  19677  dvnadd  19683  dvcj  19704  dvmptfsum  19727  c1liplem1  19748  evl1rhm  19817  pf1mpf  19840  tdeglem4  19851  mdegldg  19857  mdegcl  19860  deg1z  19878  plypf1  19999  0dgr  20032  coemulc  20041  plyremlem  20089  qaa  20108  aannenlem2  20114  aaliou3lem2  20128  aaliou3lem8  20130  aaliou3lem6  20133  ulmval  20164  abelth  20225  reeff1olem  20230  reeff1o  20231  ef2kpi  20254  sinperlem  20256  sin2kpi  20259  cos2kpi  20260  sinhalfpip  20268  sinhalfpim  20269  coshalfpip  20270  coshalfpim  20271  sincosq1sgn  20274  sinq12gt0  20283  sincos6thpi  20291  sinkpi  20295  sineq0  20297  resinf1o  20306  tanord1  20307  tanord  20308  eflog  20342  logef  20344  dvrelog  20396  dvlog  20410  efopn  20417  0cxp  20425  cxpge0  20442  cxplea  20455  root1id  20506  isosctrlem1  20530  isosctrlem2  20531  asinlem  20576  asinlem2  20577  asinf  20580  atandm2  20585  asinneg  20594  efiasin  20596  sinasin  20597  asinbnd  20607  asinrebnd  20609  cosasin  20612  atans2  20639  leibpilem1  20648  leibpilem2  20649  leibpisum  20651  log2cnv  20652  log2tlbnd  20653  log2ublem2  20655  ftalem3  20725  ftalem5  20727  basellem1  20731  basellem2  20732  basellem4  20734  basellem5  20735  basellem8  20738  0sgm  20795  ppieq0  20827  chpeq0  20860  chteq0  20861  chtublem  20863  chtub  20864  pcbcctr  20928  bcp1ctr  20931  bclbnd  20932  bposlem1  20936  bposlem2  20937  m1lgs  21014  chebbnd1lem1  21031  chtppilim  21037  pntrsumbnd2  21129  pntibnd  21155  qrngneg  21185  ostth  21201  umgrafi  21225  usgraedg4  21273  cusgrarn  21335  wlkntrllem5  21418  constr1trl  21437  1pthon  21440  constr2trl  21447  2pthonlem2  21449  3v3e3cycl1  21480  constr3trllem2  21487  constr3pthlem1  21491  constr3pthlem3  21493  4cycl4v4e  21502  4cycl4dv4e  21504  0conngra  21510  iseupa  21536  grpo2grp  21671  issubgoi  21747  addinv  21789  ablomul  21792  mulid  21793  rngoi  21817  drngoi  21844  rngoablo2  21859  rngoidmlem  21860  vafval  21931  smfval  21933  0vfval  21934  nvop2  21936  vsfval  21963  nvop  22015  cnnvdemo  22020  imsmetlem  22031  lnocoi  22107  nmoubi  22122  nmoub3i  22123  nmlno0lem  22143  nmlnogt0  22147  nmblolbii  22149  blocnilem  22154  phop  22168  ipasslem1  22181  ipasslem2  22182  ipasslem4  22184  ipasslem5  22185  ipasslem9  22188  ipasslem11  22190  siilem1  22201  siii  22203  ipblnfi  22206  ip2eqi  22207  ubthlem1  22221  ubthlem2  22222  ubthlem3  22223  minvecolem3  22227  htthlem  22269  axhvass-zf  22336  axhvaddid-zf  22338  axhvmulid-zf  22340  axhvmulass-zf  22341  axhvdistr1-zf  22342  axhvdistr2-zf  22343  axhvmul0-zf  22344  axhis2-zf  22347  axhis3-zf  22348  axhcompl-zf  22350  hvsubf  22367  hvsubcl  22369  hv2neg  22379  hvaddsubval  22384  hvsub4  22388  hvaddsub12  22389  hvpncan  22390  hvaddsubass  22392  hvsubass  22395  hvsubdistr1  22400  hvaddeq0  22420  hvsubcan  22425  his2sub  22443  hi01  22447  normneg  22495  hilablo  22511  hilnormi  22514  bcsiALT  22530  hhssnv  22613  occllem  22654  spanval  22684  spancl  22687  shslubi  22736  ococin  22759  pjcli  22768  pjhcli  22769  h1de2ctlem  22906  spanunsni  22930  cm0  22960  chscllem2  22989  spansncvi  23003  pjjsi  23051  pjrni  23053  pjdsi  23063  pjoi0i  23069  mayete3i  23079  mayete3iOLD  23080  ho0val  23102  hocoi  23116  homulid2  23152  hosubneg  23159  hosubdi  23160  honegsubdi  23162  honegsubdi2  23163  hosub4  23165  hoaddsubass  23167  hosubsub4  23170  eigrei  23186  eigposi  23188  eigorthi  23189  nmopsetretHIL  23216  adj1  23285  lnopeq0i  23359  hmopd  23374  nmbdoplbi  23376  nmcexi  23378  nmcoplbi  23380  lnopconi  23386  nmbdfnlbi  23401  nmcfnlbi  23404  lnfnconi  23407  nmopadjlei  23440  nmopcoi  23447  branmfn  23457  cnvbraval  23462  cnvbracl  23463  cnvbrabra  23464  bracnvbra  23465  leoppos  23478  opsqrlem1  23492  pjnmopi  23500  hmopidmpji  23504  pjnormssi  23520  pjtoi  23531  pjadj3  23540  pjclem4a  23550  pj3lem1  23558  pj3si  23559  strlem4  23606  strlem5  23607  hstrlem4  23614  hstrlem5  23615  jplem1  23620  mdslle1i  23669  mdslle2i  23670  mdslj1i  23671  mdslj2i  23672  mdsl1i  23673  mdsl2i  23674  mdslmd1lem1  23677  mdslmd1lem2  23678  mdslmd2i  23682  csmdsymi  23686  mdexchi  23687  elat2  23692  shatomici  23710  shatomistici  23713  chrelati  23716  chrelat2i  23717  cvbr4i  23719  cvexchlem  23720  atomli  23734  atordi  23736  chirredlem4  23745  atcvat3i  23748  atcvat4i  23749  atabsi  23753  mdsymlem1  23755  mdsymlem3  23757  mdsymlem5  23759  sumdmdlem2  23771  cdj1i  23785  abrexdomjm  23833  disjdifprg  23862  iundisj2f  23874  xppreima  23902  xrofsup  23963  iundisj2fi  23992  xgtpnf  24016  tpr2rico  24115  mndpluscn  24117  qqhcn  24175  indf1ofs  24220  esumeq2  24230  esumpcvgval  24265  hasheuni  24272  esumcvg  24273  prsiga  24311  measbasedom  24352  measvuni  24363  cntmeas  24375  volmeas  24382  dya2ub  24415  dya2icoseg  24422  ballotlemfc0  24530  zetacvg  24579  eflgam  24609  subfacval2  24653  subfaclim  24654  erdszelem5  24661  erdszelem8  24664  cvmsss2  24741  cvmlift2lem1  24769  cvmlift2lem12  24781  cvmliftphtlem  24784  ghomgrpilem2  24877  zmodid2  24894  relexp1  24911  mulge0b  24971  prodfclim1  25001  prodsn  25066  fallrisefac  25110  risefacfac  25118  dfpo2  25137  dfon2lem3  25166  dfon2lem7  25170  rdgprc  25176  elpredim  25201  soseq  25279  wfrlem10  25290  wfrlem16  25296  sltirr  25349  slttr  25350  slttri  25352  slttrieq2  25353  bdayelon  25359  nocvxminlem  25369  nocvxmin  25370  nobndlem1  25371  nobndlem2  25372  nofulllem5  25385  fnimage  25493  imageval  25494  fullfunfv  25511  altopeq2  25524  brbtwn2  25559  colinearalglem4  25563  ax5seglem1  25582  ax5seglem2  25583  ax5seglem5  25587  axbtwnid  25593  axlowdimlem9  25604  axlowdimlem12  25607  axlowdimlem16  25611  axlowdimlem17  25612  axcontlem2  25619  axcontlem7  25624  bpoly0  25811  bpoly1  25812  bpoly2  25818  bpoly3  25819  bpoly4  25820  fsumcube  25821  limsucncmpi  25910  onint1  25914  ovoliunnfl  25954  voliunnfl  25956  itg2addnc  25960  opnrebl2  26016  comppfsc  26079  abrexdom  26124  incsequz2  26145  isbnd2  26184  totbndbnd  26190  prdsbnd  26194  cntotbnd  26197  heiborlem3  26214  heiborlem6  26217  heibor  26222  repwsmet  26235  rrntotbnd  26237  isdrngo1  26264  iscrngo2  26300  prtlem400  26411  ismrc  26447  mzpresrename  26499  mzpcompact2lem  26500  eluzrabdioph  26558  rencldnfilem  26573  reglogltb  26646  reglogleb  26647  rmspecnonsq  26662  rmspecfund  26664  rmspecpos  26671  rmxypos  26704  jm3.1  26783  ttac  26799  pw2f1ocnv  26800  aomclem6  26826  pwssplit4  26861  frlmpws  26888  frlmlss  26889  frlmpwsfi  26890  frlmsca  26891  frlmbas  26893  frlmbasf  26898  uvcff  26910  frlmpwfi  26932  numinfctb  26938  isnumbasgrplem3  26940  islinds2  26953  islindf4  26978  hausgraph  27201  dvconstbi  27221  rabexgf  27364  aovprc  27722  aovrcl  27723  sinh-conventional  27829  dpfrac1  27862  sgnp  27867  elogb  27879  eel000cT  28148  eelT00  28150  eel00000  28176  eel00cT  28224  bnj519  28442  bnj157  28569  bnj546  28606  cdleme31fv  30505
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