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

Theorem mp3an 1307
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 1294 . 2  |-  ( ( ps  /\  ch )  ->  th )
61, 2, 5mp2an 665 1  |-  th
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 958
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 960
This theorem is referenced by:  vtocl3  3015  raltp  3919  rextp  3920  funopg  5438  ftp  5880  caovass  6252  caovdi  6271  ordom  6474  ofmres  6562  omopthlem1  7082  omopthlem2  7083  omopthi  7084  xpcomen  7390  unfilem3  7566  hartogs  7746  card2on  7757  unwf  8005  tskwe  8108  alephsmo  8260  dfac4  8280  dfac2a  8287  ackbij1lem5  8381  ackbij1lem13  8389  axdc2lem  8605  axcclem  8614  ondomon  8715  cfpwsdom  8736  pwfseqlem2  8814  pwfseqlem3  8815  1lt2pi  9062  addassi  9382  mulassi  9383  adddii  9384  adddiri  9385  lttri  9488  lelttri  9489  ltletri  9490  letri  9491  ltadd2i  9493  mul02lem2  9534  addid1  9537  addcani  9550  addcan2i  9551  mul12i  9552  mul32i  9553  add12i  9575  add32i  9576  subaddi  9683  subadd2i  9684  subsub23i  9686  addsubassi  9687  addsubi  9688  subcani  9689  subcan2i  9690  pnncani  9691  subdii  9781  subdiri  9782  ltadd1i  9882  leadd1i  9883  leadd2i  9884  ltsubaddi  9885  lesubaddi  9886  ltsubadd2i  9887  lesubadd2i  9888  ltaddsubi  9889  mulcani  9963  div23i  10077  div11i  10078  1mhlfehlf  10532  halfpm6th  10534  addex  10977  mulex  10978  unirnioo  11377  ioorebas  11379  uzenom  11771  nnenom  11786  m1expcl2  11871  i4  11952  expnass  11955  faclbnd4lem1  12053  bcn1  12073  ccatfn  12256  cats1fvn  12469  cats1fv  12470  cats1cat  12472  abs3difi  12880  0.999...  13324  geoihalfsum  13325  ef01bndlem  13451  cos1bnd  13454  cos2bnd  13455  sin4lt0  13462  rpnnen2lem3  13482  rpnnen2lem11  13490  rpnnen  13492  rexpen  13493  aleph1irr  13511  divalglem2  13582  ndvdsi  13597  gcdaddmlem  13695  bezout  13709  3prm  13763  dec2dvds  14075  modxai  14080  modsubi  14084  gcdi  14085  numexp2x  14091  prdsval  14376  prdsds  14385  mreexexd  14569  plusffval  15410  pmtrprfval  15973  m1expaddsub  15984  0frgp  16256  staffval  16856  scaffval  16890  cnfldcj  17669  cnfldds  17672  xrsadd  17677  xrsmul  17678  xrsds  17700  zring0  17735  zrng0  17741  cnmsgnsubg  17849  psgninv  17854  re0g  17884  ipffval  17919  ocvfval  17933  frlmbas  18022  frlmbasOLD  18023  mdetrlin  18251  mdetunilem9  18268  leordtval2  18658  iscnp2  18685  utop3cls  19668  nmfval  20023  nmoffn  20132  nmofval  20135  icccld  20188  addcnlem  20282  iimulcn  20352  icopnfhmeo  20357  iccpnfcnv  20358  iccpnfhmeo  20359  xrhmeo  20360  xrhmph  20361  oprpiece1res1  20365  oprpiece1res2  20366  ishtpy  20386  pcoass  20438  tchex  20574  cnfldcusp  20711  resscdrg  20712  reust  20727  recusp  20728  vitalilem4  20933  vitalilem5  20934  mbfdm  20948  dveflem  21293  dvlipcn  21308  c1lip2  21312  dgrid  21616  iaa  21676  abelthlem3  21783  abelthlem5  21785  abelth  21791  efcn  21793  sinhalfpilem  21810  sincosq1lem  21844  sincosq4sgn  21848  tangtx  21852  sincos4thpi  21860  sincos6thpi  21862  pige3  21864  relogcn  21968  dvlog2lem  21982  dvlog2  21983  logtayl  21990  logtayl2  21992  cxpsqrlem  22032  cxpsqr  22033  cxpcn2  22069  cxpcn3  22071  ang180lem1  22090  ang180lem2  22091  1cubrlem  22121  mcubic  22127  quart1lem  22135  quart1  22136  reasinsin  22176  atancj  22190  efiatan  22192  atantan  22203  atanbndlem  22205  atan1  22208  atancn  22216  atantayl2  22218  log2cnv  22224  log2tlbnd  22225  log2ublem1  22226  log2ublem2  22227  log2ub  22229  efrlim  22248  scvxcvx  22264  1sgm2ppw  22424  ppiub  22428  bclbnd  22504  bposlem8  22515  lgsdir2lem1  22547  lgsdir2lem5  22551  lgseisenlem1  22573  lgseisenlem2  22574  lgsquadlem1  22578  chebbnd1  22606  dchrvmasumlem2  22632  trgcgrg  22848  ax5seglem7  23004  axlowdimlem6  23016  axlowdimlem8  23018  axlowdimlem11  23021  cusgrasizeindb1  23202  3v3e3cycl1  23353  constr3lem2  23355  constr3lem5  23357  constr3trllem5  23363  vdegp1ai  23428  ex-fl  23477  0vfval  23807  smcnlem  23915  lnocoi  23980  nmlno0lem  24016  nmblolbii  24022  blocnilem  24027  blocni  24028  cncph  24042  isph  24045  ip0i  24048  ip1ilem  24049  ip2i  24051  ipdirilem  24052  ipasslem7  24059  ipasslem8  24060  ipasslem9  24061  ipasslem10  24062  ipasslem11  24063  ip2dii  24067  pythi  24073  siilem1  24074  siilem2  24075  siii  24076  hvmulassi  24271  hvmulcomi  24272  hvdistr1i  24276  hvsubdistr1i  24277  hvassi  24278  hvadd32i  24279  hvsubassi  24280  hvsub32i  24281  normlem0  24334  normlem8  24342  normlem9  24343  bcseqi  24345  polid2i  24382  hhph  24403  hlim0  24461  shscli  24543  shlessi  24603  shlej1i  24604  omlsilem  24628  shlubi  24641  h1de2i  24779  pjadjii  24900  pjaddii  24901  pjmulii  24903  pjdifnormii  24909  pjcji  24910  hoaddsubassi  25047  eigrei  25061  eigposi  25063  eigorthi  25064  adj0  25221  lnopeq0lem1  25232  lnopunilem1  25237  lnophmlem2  25244  nmcexi  25253  nmcopexi  25254  lnfn0i  25269  nmcfnexi  25278  mdexchi  25562  xppreima2  25789  elxrge02  25930  xrge0adddir  25979  xrnarchi  26025  nn0srg  26063  rge0srg  26064  xrge0slmod  26166  raddcn  26213  xrge0iifcnv  26217  xrge0iifiso  26219  xrge0iifhmeo  26220  xrge0iifhom  26221  xrge0iifmhm  26223  xrge0mulc1cn  26225  lmlimxrge0  26232  pnfneige0  26235  lmxrge0  26236  zringnm  26242  zzsnmOLD  26244  cnzh  26253  rezh  26254  qqh0  26267  qqh1  26268  qqhucn  26275  esumpinfval  26376  hashf2  26387  esumcvg  26389  br2base  26538  sxbrsigalem3  26541  dya2iocbrsiga  26544  dya2icobrsiga  26545  sxbrsigalem1  26554  sxbrsigalem2  26555  sxbrsigalem4  26556  sxbrsigalem5  26557  sxbrsiga  26559  ballotlem2  26719  ballotlem4  26729  ballotlemi1  26733  ballotth  26768  sgnclre  26770  signstf  26815  subfacp1lem1  26915  subfacp1lem6  26921  kur14lem6  26947  cvmliftlem4  27025  problem4  27149  fununiq  27428  fvtransport  27910  bpoly3  28048  cos2h  28267  tan2h  28268  ismblfin  28276  mbfposadd  28283  ftc1anclem5  28315  asindmre  28323  dvasin  28324  dvacos  28325  rrnval  28570  rabren3dioph  28999  jm2.27dlem2  29204  rmydioph  29208  rmxdioph  29210  expdiophlem2  29216  expdioph  29217  arearect  29436  areaquad  29437  lhe4.4ex1a  29448  itgsin0pilem1  29636  stoweidlem13  29654  wallispilem2  29707  wallispilem4  29709  wallispi2lem1  29712  stirlinglem13  29727  erclwwlktr  30331  erclwwlkntr  30347  0egra0rgra  30395  usg2spot2nb  30504  zlmodzxz0  30587  zlmodzxzequa  30747  zlmodzxzequap  30750  zlmodzxzldeplem3  30753  ax6e2ndeqALT  31369  sineq0ALT  31375  bj-pirp  32108  bj-minftyccb  32128  dihjatcclem4  34639  pirp  35186  taupilem2  35189
  Copyright terms: Public domain W3C validator