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  3105  sbnfc2  3154  ssdifss  3320  uneqdifeq  3555  elssuni  3871  riinrab  3993  difexg  4178  rabexg  4180  abssexg  4211  snexALT  4212  copsexg  4268  oteqex  4275  trsuc  4492  oneli  4516  on0eqel  4526  unexb  4536  opeluu  4542  rabxfr  4572  reuhyp  4578  onminesb  4605  onminsb  4606  onintrab  4608  onnminsb  4611  limuni3  4659  tfindsg2  4668  dfom2  4674  brrelexi  4745  brrelex2i  4746  xpss2  4812  opabid2  4831  eliunxp  4839  releldmi  4931  relelrni  4932  dmexg  4955  rnexg  4956  elres  5006  resexg  5010  relbrcnvg  5068  brcodir  5078  soirri  5085  sotri  5086  sotri2  5088  sotri3  5089  soirriOLD  5090  sotriOLD  5091  dfrel2  5140  coi1  5204  fco  5414  fssres  5424  fabexg  5438  fvco4i  5613  fvopab3g  5614  mpteqb  5630  fvimacnv  5656  ffvelrni  5680  fvconst2  5745  resfunexgALT  5754  mptexg  5761  oprabid  5898  ovprc  5901  ndmov  6020  caovcl  6030  caovass  6036  caovdi  6055  ofexg  6098  ot1stg  6150  ot2ndg  6151  ot3rdg  6152  fo1stres  6159  fo2ndres  6160  elopabi  6201  mpt2exxg  6211  frxp  6241  brtpos  6259  rntpos  6263  iunonOLD  6372  smores  6385  tfrlem9a  6418  tfrlem14  6423  tz7.44-2  6436  tz7.44-3  6437  rdgsucmptf  6457  rdglim2  6461  frsucmpt  6466  tz7.48lem  6469  tz7.48-2  6470  tz7.48-1  6471  tz7.49  6473  seqomlem4  6481  abianfplem  6486  abianfp  6487  ordgt0ge1  6512  oe0m  6533  oesuclem  6540  oacl  6550  omcl  6551  oecl  6552  oa0r  6553  om0r  6554  om1r  6557  oe1m  6559  oawordeulem  6568  oaass  6575  odi  6593  omass  6594  oneo  6595  oen0  6600  oewordi  6605  oewordri  6606  oeoalem  6610  oeoa  6611  oeoelem  6612  oeoe  6613  nna0r  6623  nnm0r  6624  nn2m  6664  nnneo  6665  nneob  6666  ecdmn0  6718  ecelqsi  6731  ectocl  6743  brecop2  6768  mapsnf1o  6873  bren  6887  f1oen  6898  ssdomg  6923  map1  6955  snfi  6957  fiprc  6958  xpsnen2g  6971  xpdom1  6977  pwdom  7029  pwen  7050  limenpsi  7052  limensuci  7053  infensuc  7055  php  7061  fineqv  7094  en1eqsn  7104  findcard3  7116  nnsdomg  7132  xpfi  7144  ixpfi2  7170  dffi2  7192  marypha1lem  7202  wofib  7276  card2on  7284  card2inf  7285  wdompwdom  7308  en2lp  7333  inf0  7338  nnsdom  7370  cantnfval2  7386  cantnfle  7388  cantnflt  7389  cnfcom  7419  zfregs  7430  r1sdom  7462  r1val1  7474  tz9.12lem3  7477  rankwflemb  7481  rankf  7482  rankr1ag  7490  rankr1bg  7491  rankr1clem  7508  rankr1c  7509  rankonidlem  7516  unbndrank  7530  rankr1b  7552  rankval4  7555  rankxplim3  7567  rankxpsuc  7568  tcrank  7570  scott0  7572  isnum3  7603  ficardom  7610  cardsdomel  7623  harsdom  7644  cardmin2  7647  infxpenlem  7657  infxpidm2  7660  finacn  7693  alephon  7712  alephcard  7713  alephordi  7717  alephsucdom  7722  alephgeom  7725  alephdom2  7730  alephprc  7742  alephfp  7751  ackbij2lem1  7861  ackbij1lem3  7864  ackbij1lem18  7879  cfeq0  7898  cfsuc  7899  cff1  7900  cflim2  7905  cofsmo  7911  fin4en1  7951  fin23lem21  7981  fin23lem28  7982  fin23lem30  7984  isf32lem5  7999  fin1a2lem4  8045  fin1a2lem13  8054  axcc2lem  8078  axdc3lem4  8095  axdc4lem  8097  zorn2lem4  8142  zorn2lem5  8143  zorn  8150  ttukeylem3  8154  axdclem  8162  brdom7disj  8172  brdom6disj  8173  cardmin  8202  infinf  8204  konigthlem  8206  alephreg  8220  pwcfsdom  8221  fpwwe2lem8  8275  fpwwe  8284  pwcdandom  8305  gchpwdom  8312  winafp  8335  wunr1om  8357  wunfi  8359  tskr1om  8405  tskr1om2  8406  inar1  8413  tskcard  8419  gruina  8456  grur1a  8457  grur1  8458  grothac  8468  indpi  8547  nqereu  8569  nqerrel  8572  ltsonq  8609  prub  8634  genpnnp  8645  distrlem4pr  8666  ltapr  8685  addcanpr  8686  suplem2pr  8693  0nsr  8717  ltsosr  8732  sqgt0sr  8744  mappsrpr  8746  map2psrpr  8748  supsrlem  8749  axpre-lttri  8803  mulid2  8852  0re  8854  axmulgt0  8913  lttri2  8920  lttri3  8921  lttri4  8922  ltnr  8931  ltnsym2  8936  ne0gt0  8941  muladd11  8998  mul02lem1  9004  cnegex2  9010  0cnALT  9057  negcl  9068  negneg  9113  mulm1  9237  lt0neg2  9297  le0neg2  9299  msqgt0i  9326  recextlem1  9414  recex  9416  recclzi  9501  recne0zi  9502  recidzi  9503  divasszi  9526  divmulzi  9527  divdirzi  9528  rerecclzi  9540  ltp1  9610  lemul1a  9626  recp1lt1  9670  squeeze0  9675  recgt0i  9677  ltmul1i  9691  ltdiv1i  9692  ltmuldivi  9693  ltmul2i  9694  lemul1i  9695  lemul2i  9696  ledivp1i  9698  ltdivp1i  9699  suprubii  9741  suprlubii  9742  suprnubii  9743  suprleubii  9744  riotaneg  9745  nnrecre  9798  nn0addcl  10015  nn0mulcl  10016  recnz  10103  peano5uzi  10116  dfuzi  10118  eluz2b1  10305  uz2m1nn  10308  zq  10338  nnrecq  10355  rpge0  10382  rpreccl  10393  rpneg  10399  mnflt  10480  pnfnlt  10483  mnfle  10486  xrlttri2  10492  xrlttri3  10493  xrltne  10510  ngtmnft  10512  qbtwnxr  10543  qsqueeze  10544  xlt0neg2  10563  xle0neg2  10565  xaddpnf2  10570  xaddmnf2  10572  xaddid2  10583  xmullem  10600  xmul02  10604  xmulpnf2  10611  xmulmnf2  10613  xmulid2  10616  xmulm1  10617  xmulge0  10620  xmulasslem  10621  xrsupsslem  10641  xrinfmsslem  10642  elioomnf  10754  fzshftral  10885  uzrdglem  11036  uzrdgfni  11037  uzrdgsuci  11039  fzennn  11046  fsequb  11053  fseqsupcl  11055  nn0ennn  11057  axdc4uzlem  11060  0exp  11153  sqgt0i  11206  sqlecan  11225  subsq2  11227  crreczi  11242  bernneq  11243  bernneq3  11245  expnbnd  11246  nn0opthlem2  11300  faclbnd  11319  faclbnd2  11320  faclbnd3  11321  faclbnd4lem1  11322  faclbnd4lem3  11324  faclbnd4lem4  11325  hashginv  11357  hashfz1  11361  hashpw  11404  hashf1lem2  11410  wrdexg  11441  ccatlid  11450  s1cl  11457  s1fv  11462  s111  11464  s1co  11504  reim  11610  imcl  11612  crim  11616  rennim  11740  cnpart  11741  resqrex  11752  sqrgt0  11760  absor  11801  absimle  11810  caubnd  11858  sqrthi  11870  sqrcli  11871  sqrgt0i  11872  sqrmsqi  11873  sqrsqi  11874  sqsqri  11875  sqrge0i  11876  absidi  11877  absnidi  11878  lo1o1  12022  serclim0  12067  fz1f1o  12199  fsum2d  12250  fsumcnv  12252  fsumabs  12275  fsumrlim  12285  fsumo1  12286  binom11  12306  harmonic  12333  mertenslem2  12357  efzval  12398  eftlub  12405  efsep  12406  ef4p  12409  efgt1  12412  eflt  12413  sinf  12420  cosf  12421  efi4p  12433  sinneg  12442  cosneg  12443  efival  12448  efmival  12449  sinhval  12450  coshval  12451  cos01gt0  12487  sin02gt0  12488  absefib  12494  efieq1re  12495  demoivre  12496  demoivreALT  12497  rpnnen2lem9  12517  0dvds  12565  dvdslelem  12589  odd2np1lem  12602  odd2np1  12603  divalglem0  12608  divalglem6  12613  divalglem9  12616  bits0e  12636  bitsfzolem  12641  bitsinv1  12649  bitsf1  12653  sadid2  12676  sadasslem  12677  sadeq  12679  bitsuz  12681  gcdcllem3  12708  gcd0id  12718  gcdid0  12719  1gcd  12732  bezoutlem1  12733  bezoutlem3  12735  isprm3  12783  odzdvds  12876  opoe  12880  omoe  12881  opeo  12882  omeo  12883  pythagtriplem12  12895  pythagtriplem13  12896  pythagtriplem14  12897  pythagtriplem16  12899  pc2dvds  12947  pockthi  12970  unbenlem  12971  1arith2  12991  vdwlem10  13053  vdwlem13  13056  prmlem1a  13124  isstruct2  13173  strle1  13255  0rest  13350  topnid  13356  pwselbasb  13403  xpscg  13476  xpsc0  13478  xpsc1  13479  brssc  13707  isfunc  13754  isfull  13800  isfth  13804  homahom  13887  homadm  13888  homacd  13889  homadmcd  13890  drsdirfi  14088  pwsdiagmhm  14461  gsumws1  14478  mulg0  14588  mulg1  14590  mulg2  14592  odlem2  14870  gexlem2  14909  efgrelexlema  15074  efgredeu  15077  dprdsubg  15275  ablfac1eulem  15323  rngidval  15359  dvdsr  15444  lbsex  15934  sralem  15946  psrbag  16128  subrgply1  16327  ply1sclid  16379  ply1coe  16384  cnfldinv  16421  gzrngunit  16453  zlpir  16460  prmirredlem  16462  prmirred  16464  zlmassa  16494  tpsexOLD  16673  tgval  16709  tgss3  16740  indistopon  16754  iscldtop  16848  restsn  16917  pnfnei  16966  2ndcdisj  17198  iskgen2  17259  fbasfip  17579  fclsrest  17735  ptcmplem2  17763  divstgpopn  17818  divstgplem  17819  stdbdmetval  18076  nmogelb  18241  iocmnfcld  18294  cnbl0  18299  cnblcld  18300  blssioo  18317  resubmet  18324  xrtgioo  18328  reconn  18349  rectbntr0  18353  fsumcn  18390  cncfmet  18428  iirev  18443  iihalf1  18445  iihalf2  18447  xrhmeo  18460  icccvx  18464  cnheibor  18469  phtpyid  18503  pcorevlem  18540  iscmet3lem2  18734  iscmet3  18735  ovolsslem  18859  ovolunlem1a  18871  ovolicc2lem4  18895  nulmbl2  18910  iundisj2  18922  dyadf  18962  dyadovol  18964  subopnmbl  18975  ismbfcn  19002  mbfimaopnlem  19026  itg1addlem4  19070  itg2leub  19105  itg2seq  19113  itgfsum  19197  limcresi  19251  cnlimc  19254  dvnff  19288  dvnadd  19294  dvcj  19315  dvmptfsum  19338  c1liplem1  19359  evl1rhm  19428  pf1mpf  19451  tdeglem4  19462  mdegldg  19468  mdegcl  19471  deg1z  19489  plypf1  19610  0dgr  19643  coemulc  19652  plyremlem  19700  qaa  19719  aannenlem2  19725  aaliou3lem2  19739  aaliou3lem8  19741  aaliou3lem6  19744  ulmval  19775  abelth  19833  reeff1olem  19838  reeff1o  19839  ef2kpi  19862  sinperlem  19864  sin2kpi  19867  cos2kpi  19868  sinhalfpip  19876  sinhalfpim  19877  coshalfpip  19878  coshalfpim  19879  sincosq1sgn  19882  sinq12gt0  19891  sincos6thpi  19899  sinkpi  19903  sineq0  19905  resinf1o  19914  tanord1  19915  tanord  19916  eflog  19949  logef  19951  dvrelog  20000  dvlog  20014  efopn  20021  0cxp  20029  cxpge0  20046  cxplea  20059  root1id  20110  isosctrlem1  20134  isosctrlem2  20135  asinlem  20180  asinlem2  20181  asinf  20184  atandm2  20189  asinneg  20198  efiasin  20200  sinasin  20201  asinbnd  20211  asinrebnd  20213  cosasin  20216  atans2  20243  leibpilem1  20252  leibpilem2  20253  leibpisum  20255  log2cnv  20256  log2tlbnd  20257  log2ublem2  20259  ftalem3  20328  ftalem5  20330  basellem1  20334  basellem2  20335  basellem4  20337  basellem5  20338  basellem8  20341  0sgm  20398  ppieq0  20430  chpeq0  20463  chteq0  20464  chtublem  20466  chtub  20467  pcbcctr  20531  bcp1ctr  20534  bclbnd  20535  bposlem1  20539  bposlem2  20540  m1lgs  20617  chebbnd1lem1  20634  chtppilim  20640  pntrsumbnd2  20732  pntibnd  20758  qrngneg  20788  ostth  20804  grpo2grp  20917  issubgoi  20993  addinv  21035  ablomul  21038  mulid  21039  rngoi  21063  drngoi  21090  rngoablo2  21105  rngoidmlem  21106  vafval  21175  smfval  21177  0vfval  21178  nvop2  21180  vsfval  21207  nvop  21259  cnnvdemo  21264  imsmetlem  21275  lnocoi  21351  nmoubi  21366  nmoub3i  21367  nmlno0lem  21387  nmlnogt0  21391  nmblolbii  21393  blocnilem  21398  phop  21412  ipasslem1  21425  ipasslem2  21426  ipasslem4  21428  ipasslem5  21429  ipasslem9  21432  ipasslem11  21434  siilem1  21445  siii  21447  ipblnfi  21450  ip2eqi  21451  ubthlem1  21465  ubthlem2  21466  ubthlem3  21467  minvecolem3  21471  htthlem  21513  axhvass-zf  21580  axhvaddid-zf  21582  axhvmulid-zf  21584  axhvmulass-zf  21585  axhvdistr1-zf  21586  axhvdistr2-zf  21587  axhvmul0-zf  21588  axhis2-zf  21591  axhis3-zf  21592  axhcompl-zf  21594  hvsubf  21611  hvsubcl  21613  hv2neg  21623  hvaddsubval  21628  hvsub4  21632  hvaddsub12  21633  hvpncan  21634  hvaddsubass  21636  hvsubass  21639  hvsubdistr1  21644  hvaddeq0  21664  hvsubcan  21669  his2sub  21687  hi01  21691  normneg  21739  hilablo  21755  hilnormi  21758  bcsiALT  21774  hhssnv  21857  occllem  21898  spanval  21928  spancl  21931  shslubi  21980  ococin  22003  pjcli  22012  pjhcli  22013  h1de2ctlem  22150  spanunsni  22174  cm0  22204  chscllem2  22233  spansncvi  22247  pjjsi  22295  pjrni  22297  pjdsi  22307  pjoi0i  22313  mayete3i  22323  mayete3iOLD  22324  ho0val  22346  hocoi  22360  homulid2  22396  hosubneg  22403  hosubdi  22404  honegsubdi  22406  honegsubdi2  22407  hosub4  22409  hoaddsubass  22411  hosubsub4  22414  eigrei  22430  eigposi  22432  eigorthi  22433  nmopsetretHIL  22460  adj1  22529  lnopeq0i  22603  hmopd  22618  nmbdoplbi  22620  nmcexi  22622  nmcoplbi  22624  lnopconi  22630  nmbdfnlbi  22645  nmcfnlbi  22648  lnfnconi  22651  nmopadjlei  22684  nmopcoi  22691  branmfn  22701  cnvbraval  22706  cnvbracl  22707  cnvbrabra  22708  bracnvbra  22709  leoppos  22722  opsqrlem1  22736  pjnmopi  22744  hmopidmpji  22748  pjnormssi  22764  pjtoi  22775  pjadj3  22784  pjclem4a  22794  pj3lem1  22802  pj3si  22803  strlem4  22850  strlem5  22851  hstrlem4  22858  hstrlem5  22859  jplem1  22864  mdslle1i  22913  mdslle2i  22914  mdslj1i  22915  mdslj2i  22916  mdsl1i  22917  mdsl2i  22918  mdslmd1lem1  22921  mdslmd1lem2  22922  mdslmd2i  22926  csmdsymi  22930  mdexchi  22931  elat2  22936  shatomici  22954  shatomistici  22957  chrelati  22960  chrelat2i  22961  cvbr4i  22963  cvexchlem  22964  atomli  22978  atordi  22980  chirredlem4  22989  atcvat3i  22992  atcvat4i  22993  atabsi  22997  mdsymlem1  22999  mdsymlem3  23001  mdsymlem5  23003  sumdmdlem2  23015  cdj1i  23029  ballotlem2  23063  ballotlemfc0  23067  ballotlem4  23073  xgtpnf  23130  abrexdomjm  23181  xppreima  23226  xrofsup  23270  tpr2rico  23311  mndpluscn  23314  mptct  23360  mptctf  23363  disjdifprg  23367  iundisj2fi  23379  iundisj2f  23381  esumeq2  23433  esumpcvgval  23461  hasheuni  23468  esumcvg  23469  dmvlsiga  23505  prsiga  23507  difelsiga  23509  measbasedom  23547  measvuni  23557  cntmeas  23568  dya2ub  23590  dya2iocseg  23594  indf1ofs  23624  zetacvg  23704  subfacval2  23733  subfaclim  23734  erdszelem5  23741  erdszelem8  23744  cvmsss2  23820  cvmlift2lem1  23848  cvmlift2lem12  23860  cvmliftphtlem  23863  umgrafi  23889  iseupa  23896  ghomgrpilem2  24008  zmodid2  24025  relexp1  24042  mulge0b  24101  faclimlem8  24124  prodfclim1  24167  dfpo2  24183  dfon2lem3  24212  dfon2lem7  24216  rdgprc  24222  elpredim  24247  soseq  24325  wfrlem10  24336  wfrlem16  24342  sltirr  24395  slttr  24396  slttri  24398  slttrieq2  24399  bdayelon  24405  nocvxminlem  24415  nocvxmin  24416  nobndlem1  24417  nobndlem2  24418  nofulllem5  24431  fnimage  24539  imageval  24540  fullfunfv  24557  altopeq2  24570  brbtwn2  24605  colinearalglem4  24609  ax5seglem1  24628  ax5seglem2  24629  ax5seglem5  24633  axbtwnid  24639  axlowdimlem9  24650  axlowdimlem12  24653  axlowdimlem16  24657  axlowdimlem17  24658  axcontlem2  24665  axcontlem7  24670  bpoly0  24857  bpoly1  24858  bpoly2  24864  bpoly3  24865  bpoly4  24866  fsumcube  24867  limsucncmpi  24956  onint1  24960  ovoliunnfl  25001  itg2addnc  25005  copsexgb  25069  prl  25270  preoref22  25332  int2pre  25340  ranncnt  25386  fprodp1  25426  seqzp2  25458  sallnei  25632  hmeogrpi  25639  qusp  25645  efilcp  25655  islimrs4  25685  bwt2  25695  altretop  25703  mslb1  25710  hdrmp  25809  domval  25826  codval  25827  idval  25828  cmpval  25829  dedalg  25846  catded  25867  valtar  25986  pwtsm  25992  subtsm  25993  subtareqbe  25994  1iskle  26092  pfsubkl  26150  pgapspf  26155  sgplpte21d1  26242  sgplpte21d2  26243  opnrebl2  26339  comppfsc  26410  abrexdom  26508  incsequz2  26562  isbnd2  26610  totbndbnd  26616  prdsbnd  26620  cntotbnd  26623  heiborlem3  26640  heiborlem6  26643  heibor  26648  repwsmet  26661  rrntotbnd  26663  isdrngo1  26690  iscrngo2  26726  prtlem400  26841  ismrc  26879  mzpresrename  26931  mzpcompact2lem  26932  eluzrabdioph  26990  rencldnfilem  27006  reglogltb  27079  reglogleb  27080  rmspecnonsq  27095  rmspecfund  27097  rmspecpos  27104  rmxypos  27137  jm3.1  27216  ttac  27232  pw2f1ocnv  27233  aomclem6  27259  pwssplit4  27294  frlmpws  27321  frlmlss  27322  frlmpwsfi  27323  frlmsca  27324  frlmbas  27326  frlmbasf  27331  uvcff  27343  frlmpwfi  27365  numinfctb  27371  isnumbasgrplem3  27373  islinds2  27386  islindf4  27411  hausgraph  27634  dvconstbi  27654  rabexgf  27798  aovprc  28156  aovrcl  28157  mpt2ndm0  28204  4fvwrd4  28220  wlkntrllem5  28349  3v3e3cycl1  28390  constr3lem4  28393  constr3trllem2  28397  constr3pthlem1  28401  constr3pthlem3  28403  4cycl4v4e  28412  4cycl4dv4e  28414  sinh-conventional  28463  dpfrac1  28496  sgnp  28501  elogb  28513  eel000cT  28783  eelT00  28785  eel001  28793  eel00cT  28859  bnj519  29080  bnj157  29207  bnj546  29244  cdleme31fv  31201
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