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

Theorem mp3an 1315
Description: An inference based on modus ponens. (Contributed by NM, 14-May-1999.)
Hypotheses
Ref Expression
mp3an.1  |-  ph
mp3an.2  |-  ps
mp3an.3  |-  ch
mp3an.4  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Assertion
Ref Expression
mp3an  |-  th

Proof of Theorem mp3an
StepHypRef Expression
1 mp3an.2 . 2  |-  ps
2 mp3an.3 . 2  |-  ch
3 mp3an.1 . . 3  |-  ph
4 mp3an.4 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
53, 4mp3an1 1302 . 2  |-  ( ( ps  /\  ch )  ->  th )
61, 2, 5mp2an 672 1  |-  th
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 965
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967
This theorem is referenced by:  vtocl3  3122  raltp  4029  rextp  4030  funopg  5548  ftp  5992  caovass  6363  caovdi  6382  ordom  6585  ofmres  6673  omopthlem1  7194  omopthlem2  7195  omopthi  7196  xpcomen  7502  unfilem3  7679  hartogs  7859  card2on  7870  unwf  8118  tskwe  8221  alephsmo  8373  dfac4  8393  dfac2a  8400  ackbij1lem5  8494  ackbij1lem13  8502  axdc2lem  8718  axcclem  8727  ondomon  8828  cfpwsdom  8849  pwfseqlem2  8927  pwfseqlem3  8928  1lt2pi  9175  addassi  9495  mulassi  9496  adddii  9497  adddiri  9498  lttri  9601  lelttri  9602  ltletri  9603  letri  9604  ltadd2i  9606  mul02lem2  9647  addid1  9650  addcani  9663  addcan2i  9664  mul12i  9665  mul32i  9666  add12i  9688  add32i  9689  subaddi  9796  subadd2i  9797  subsub23i  9799  addsubassi  9800  addsubi  9801  subcani  9802  subcan2i  9803  pnncani  9804  subdii  9894  subdiri  9895  ltadd1i  9995  leadd1i  9996  leadd2i  9997  ltsubaddi  9998  lesubaddi  9999  ltsubadd2i  10000  lesubadd2i  10001  ltaddsubi  10002  mulcani  10076  div23i  10190  div11i  10191  1mhlfehlf  10645  halfpm6th  10647  addex  11090  mulex  11091  unirnioo  11490  ioorebas  11492  uzenom  11888  nnenom  11903  m1expcl2  11988  i4  12069  expnass  12072  faclbnd4lem1  12170  bcn1  12190  ccatfn  12374  cats1fvn  12587  cats1fv  12588  cats1cat  12590  abs3difi  12998  0.999...  13443  geoihalfsum  13444  ef01bndlem  13570  cos1bnd  13573  cos2bnd  13574  sin4lt0  13581  rpnnen2lem3  13601  rpnnen2lem11  13609  rpnnen  13611  rexpen  13612  aleph1irr  13630  divalglem2  13701  ndvdsi  13716  gcdaddmlem  13814  bezout  13828  3prm  13882  dec2dvds  14194  modxai  14199  modsubi  14203  gcdi  14204  numexp2x  14210  prdsval  14495  prdsds  14504  mreexexd  14688  plusffval  15529  pmtrprfval  16095  m1expaddsub  16106  0frgp  16380  staffval  17038  scaffval  17072  cnfldcj  17934  cnfldds  17937  xrsadd  17942  xrsmul  17943  xrsds  17965  nn0srg  17990  rge0srg  17991  zring0  18002  zrng0  18008  cnmsgnsubg  18116  psgninv  18121  re0g  18151  ipffval  18186  ocvfval  18200  frlmbas  18289  frlmbasOLD  18290  mdetrlin  18524  mdetunilem9  18542  leordtval2  18932  iscnp2  18959  utop3cls  19942  nmfval  20297  nmoffn  20406  nmofval  20409  icccld  20462  addcnlem  20556  iimulcn  20626  icopnfhmeo  20631  iccpnfcnv  20632  iccpnfhmeo  20633  xrhmeo  20634  xrhmph  20635  oprpiece1res1  20639  oprpiece1res2  20640  ishtpy  20660  pcoass  20712  tchex  20848  cnfldcusp  20985  resscdrg  20986  reust  21001  recusp  21002  vitalilem4  21207  vitalilem5  21208  mbfdm  21222  dveflem  21567  dvlipcn  21582  c1lip2  21586  dgrid  21847  iaa  21907  abelthlem3  22014  abelthlem5  22016  abelth  22022  efcn  22024  sinhalfpilem  22041  sincosq1lem  22075  sincosq4sgn  22079  tangtx  22083  sincos4thpi  22091  sincos6thpi  22093  pige3  22095  relogcn  22199  dvlog2lem  22213  dvlog2  22214  logtayl  22221  logtayl2  22223  cxpsqrlem  22263  cxpsqr  22264  cxpcn2  22300  cxpcn3  22302  ang180lem1  22321  ang180lem2  22322  1cubrlem  22352  mcubic  22358  quart1lem  22366  quart1  22367  reasinsin  22407  atancj  22421  efiatan  22423  atantan  22434  atanbndlem  22436  atan1  22439  atancn  22447  atantayl2  22449  log2cnv  22455  log2tlbnd  22456  log2ublem1  22457  log2ublem2  22458  log2ub  22460  efrlim  22479  scvxcvx  22495  1sgm2ppw  22655  ppiub  22659  bclbnd  22735  bposlem8  22746  lgsdir2lem1  22778  lgsdir2lem5  22782  lgseisenlem1  22804  lgseisenlem2  22805  lgsquadlem1  22809  chebbnd1  22837  dchrvmasumlem2  22863  trgcgrg  23086  ax5seglem7  23316  axlowdimlem6  23328  axlowdimlem8  23330  axlowdimlem11  23333  cusgrasizeindb1  23514  3v3e3cycl1  23665  constr3lem2  23667  constr3lem5  23669  constr3trllem5  23675  vdegp1ai  23740  ex-fl  23789  0vfval  24119  smcnlem  24227  lnocoi  24292  nmlno0lem  24328  nmblolbii  24334  blocnilem  24339  blocni  24340  cncph  24354  isph  24357  ip0i  24360  ip1ilem  24361  ip2i  24363  ipdirilem  24364  ipasslem7  24371  ipasslem8  24372  ipasslem9  24373  ipasslem10  24374  ipasslem11  24375  ip2dii  24379  pythi  24385  siilem1  24386  siilem2  24387  siii  24388  hvmulassi  24583  hvmulcomi  24584  hvdistr1i  24588  hvsubdistr1i  24589  hvassi  24590  hvadd32i  24591  hvsubassi  24592  hvsub32i  24593  normlem0  24646  normlem8  24654  normlem9  24655  bcseqi  24657  polid2i  24694  hhph  24715  hlim0  24773  shscli  24855  shlessi  24915  shlej1i  24916  omlsilem  24940  shlubi  24953  h1de2i  25091  pjadjii  25212  pjaddii  25213  pjmulii  25215  pjdifnormii  25221  pjcji  25222  hoaddsubassi  25359  eigrei  25373  eigposi  25375  eigorthi  25376  adj0  25533  lnopeq0lem1  25544  lnopunilem1  25549  lnophmlem2  25556  nmcexi  25565  nmcopexi  25566  lnfn0i  25581  nmcfnexi  25590  mdexchi  25874  xppreima2  26099  xrge0infss  26187  elxrge02  26241  xrge0adddir  26289  xrnarchi  26335  xrge0slmod  26446  raddcn  26493  xrge0iifcnv  26497  xrge0iifiso  26499  xrge0iifhmeo  26500  xrge0iifhom  26501  xrge0iifmhm  26503  xrge0mulc1cn  26505  lmlimxrge0  26512  pnfneige0  26515  lmxrge0  26516  zringnm  26522  zzsnmOLD  26524  cnzh  26533  rezh  26534  qqh0  26547  qqh1  26548  qqhucn  26555  esumpinfval  26656  hashf2  26667  esumcvg  26669  br2base  26818  sxbrsigalem3  26821  dya2iocbrsiga  26824  dya2icobrsiga  26825  sxbrsigalem1  26834  sxbrsigalem2  26835  sxbrsigalem4  26836  sxbrsigalem5  26837  sxbrsiga  26839  oms0  26844  ballotlem2  27005  ballotlem4  27015  ballotlemi1  27019  ballotth  27054  sgnclre  27056  signstf  27101  subfacp1lem1  27201  subfacp1lem6  27207  kur14lem6  27233  cvmliftlem4  27311  problem4  27435  fununiq  27715  fvtransport  28197  bpoly3  28335  cos2h  28561  tan2h  28562  ismblfin  28570  mbfposadd  28577  ftc1anclem5  28609  asindmre  28617  dvasin  28618  dvacos  28619  rrnval  28864  rabren3dioph  29292  jm2.27dlem2  29497  rmydioph  29501  rmxdioph  29503  expdiophlem2  29509  expdioph  29510  arearect  29729  areaquad  29730  lhe4.4ex1a  29741  itgsin0pilem1  29928  stoweidlem13  29946  wallispilem2  29999  wallispilem4  30001  wallispi2lem1  30004  stirlinglem13  30019  erclwwlktr  30623  erclwwlkntr  30639  0egra0rgra  30687  usg2spot2nb  30796  zlmodzxz0  30891  zlmodzxzequa  31145  zlmodzxzequap  31148  zlmodzxzldeplem3  31151  ax6e2ndeqALT  31967  sineq0ALT  31973  bj-pirp  32834  bj-minftyccb  32854  dihjatcclem4  35372  pirp  35919  taupilem2  35922
  Copyright terms: Public domain W3C validator