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

Theorem mp3an 1319
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 1306 . 2  |-  ( ( ps  /\  ch )  ->  th )
61, 2, 5mp2an 672 1  |-  th
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 968
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 970
This theorem is referenced by:  vtocl3  3160  raltp  4075  rextp  4076  funopg  5611  ftp  6063  caovass  6450  caovdi  6469  ordom  6680  ofmres  6770  omopthlem1  7294  omopthlem2  7295  omopthi  7296  xpcomen  7598  unfilem3  7775  hartogs  7958  card2on  7969  unwf  8217  tskwe  8320  alephsmo  8472  dfac4  8492  dfac2a  8499  ackbij1lem5  8593  ackbij1lem13  8601  axdc2lem  8817  axcclem  8826  ondomon  8927  cfpwsdom  8948  pwfseqlem2  9026  pwfseqlem3  9027  1lt2pi  9272  addassi  9593  mulassi  9594  adddii  9595  adddiri  9596  lttri  9699  lelttri  9700  ltletri  9701  letri  9702  ltadd2i  9704  mul02lem2  9745  addid1  9748  addcani  9761  addcan2i  9762  mul12i  9763  mul32i  9764  add12i  9786  add32i  9787  subaddi  9895  subadd2i  9896  subsub23i  9898  addsubassi  9899  addsubi  9900  subcani  9901  subcan2i  9902  pnncani  9903  subdii  9994  subdiri  9995  ltadd1i  10096  leadd1i  10097  leadd2i  10098  ltsubaddi  10099  lesubaddi  10100  ltsubadd2i  10101  lesubadd2i  10102  ltaddsubi  10103  mulcani  10177  div23i  10291  div11i  10292  1mhlfehlf  10747  halfpm6th  10749  addex  11207  mulex  11208  unirnioo  11613  ioorebas  11615  uzenom  12031  nnenom  12046  m1expcl2  12144  i4  12225  expnass  12228  faclbnd4lem1  12326  bcn1  12346  ccatfn  12543  cats1fvn  12773  cats1fv  12774  cats1cat  12776  abs3difi  13190  0.999...  13642  geoihalfsum  13643  ef01bndlem  13769  cos1bnd  13772  cos2bnd  13773  sin4lt0  13780  rpnnen2lem3  13800  rpnnen2lem11  13808  rpnnen  13810  rexpen  13811  aleph1irr  13829  divalglem2  13901  ndvdsi  13916  gcdaddmlem  14014  bezout  14028  3prm  14082  dec2dvds  14397  modxai  14402  modsubi  14406  gcdi  14407  numexp2x  14413  prdsval  14699  prdsds  14708  mreexexd  14892  plusffval  15733  pmtrprfval  16301  m1expaddsub  16312  0frgp  16586  staffval  17272  scaffval  17306  cnfldcj  18191  cnfldds  18194  xrsadd  18199  xrsmul  18200  xrsds  18222  nn0srg  18247  rge0srg  18248  zring0  18259  zrng0  18265  cnmsgnsubg  18373  psgninv  18378  re0g  18408  ipffval  18443  ocvfval  18457  frlmbas  18546  frlmbasOLD  18547  mdetrlin  18864  mdetunilem9  18882  leordtval2  19472  iscnp2  19499  utop3cls  20482  nmfval  20837  nmoffn  20946  nmofval  20949  icccld  21002  addcnlem  21096  iimulcn  21166  icopnfhmeo  21171  iccpnfcnv  21172  iccpnfhmeo  21173  xrhmeo  21174  xrhmph  21175  oprpiece1res1  21179  oprpiece1res2  21180  ishtpy  21200  pcoass  21252  tchex  21388  cnfldcusp  21525  resscdrg  21526  reust  21541  recusp  21542  vitalilem4  21748  vitalilem5  21749  mbfdm  21763  dveflem  22108  dvlipcn  22123  c1lip2  22127  dgrid  22388  iaa  22448  abelthlem3  22555  abelthlem5  22557  abelth  22563  efcn  22565  sinhalfpilem  22582  sincosq1lem  22616  sincosq4sgn  22620  tangtx  22624  sincos4thpi  22632  sincos6thpi  22634  pige3  22636  relogcn  22740  dvlog2lem  22754  dvlog2  22755  logtayl  22762  logtayl2  22764  cxpsqrlem  22804  cxpsqr  22805  cxpcn2  22841  cxpcn3  22843  ang180lem1  22862  ang180lem2  22863  1cubrlem  22893  mcubic  22899  quart1lem  22907  quart1  22908  reasinsin  22948  atancj  22962  efiatan  22964  atantan  22975  atanbndlem  22977  atan1  22980  atancn  22988  atantayl2  22990  log2cnv  22996  log2tlbnd  22997  log2ublem1  22998  log2ublem2  22999  log2ub  23001  efrlim  23020  scvxcvx  23036  1sgm2ppw  23196  ppiub  23200  bclbnd  23276  bposlem8  23287  lgsdir2lem1  23319  lgsdir2lem5  23323  lgseisenlem1  23345  lgseisenlem2  23346  lgsquadlem1  23350  chebbnd1  23378  dchrvmasumlem2  23404  trgcgrg  23627  ax5seglem7  23907  axlowdimlem6  23919  axlowdimlem8  23921  axlowdimlem11  23924  cusgrasizeindb1  24133  3v3e3cycl1  24306  constr3lem2  24308  constr3lem5  24310  constr3trllem5  24316  erclwwlktr  24477  erclwwlkntr  24489  0egra0rgra  24598  vdegp1ai  24646  ex-fl  24695  0vfval  25025  smcnlem  25133  lnocoi  25198  nmlno0lem  25234  nmblolbii  25240  blocnilem  25245  blocni  25246  cncph  25260  isph  25263  ip0i  25266  ip1ilem  25267  ip2i  25269  ipdirilem  25270  ipasslem7  25277  ipasslem8  25278  ipasslem9  25279  ipasslem10  25280  ipasslem11  25281  ip2dii  25285  pythi  25291  siilem1  25292  siilem2  25293  siii  25294  hvmulassi  25489  hvmulcomi  25490  hvdistr1i  25494  hvsubdistr1i  25495  hvassi  25496  hvadd32i  25497  hvsubassi  25498  hvsub32i  25499  normlem0  25552  normlem8  25560  normlem9  25561  bcseqi  25563  polid2i  25600  hhph  25621  hlim0  25679  shscli  25761  shlessi  25821  shlej1i  25822  omlsilem  25846  shlubi  25859  h1de2i  25997  pjadjii  26118  pjaddii  26119  pjmulii  26121  pjdifnormii  26127  pjcji  26128  hoaddsubassi  26265  eigrei  26279  eigposi  26281  eigorthi  26282  adj0  26439  lnopeq0lem1  26450  lnopunilem1  26455  lnophmlem2  26462  nmcexi  26471  nmcopexi  26472  lnfn0i  26487  nmcfnexi  26496  mdexchi  26780  xppreima2  27010  xrge0infss  27098  elxrge02  27146  xrge0adddir  27194  xrnarchi  27240  xrge0slmod  27347  raddcn  27397  xrge0iifcnv  27401  xrge0iifiso  27403  xrge0iifhmeo  27404  xrge0iifhom  27405  xrge0iifmhm  27407  xrge0mulc1cn  27409  lmlimxrge0  27416  pnfneige0  27419  lmxrge0  27420  zringnm  27426  zzsnmOLD  27428  cnzh  27437  rezh  27438  qqh0  27451  qqh1  27452  qqhucn  27459  esumpinfval  27569  hashf2  27580  esumcvg  27582  br2base  27730  sxbrsigalem3  27733  dya2iocbrsiga  27736  dya2icobrsiga  27737  sxbrsigalem1  27746  sxbrsigalem2  27747  sxbrsigalem4  27748  sxbrsigalem5  27749  sxbrsiga  27751  oms0  27756  ballotlem2  27917  ballotlem4  27927  ballotlemi1  27931  ballotth  27966  sgnclre  27968  signstf  28013  subfacp1lem1  28113  subfacp1lem6  28119  kur14lem6  28145  cvmliftlem4  28223  problem4  28347  fununiq  28627  fvtransport  29109  bpoly3  29247  cos2h  29474  tan2h  29475  ismblfin  29483  mbfposadd  29490  ftc1anclem5  29522  asindmre  29530  dvasin  29531  dvacos  29532  rrnval  29777  rabren3dioph  30204  jm2.27dlem2  30409  rmydioph  30413  rmxdioph  30415  expdiophlem2  30421  expdioph  30422  arearect  30641  areaquad  30642  lhe4.4ex1a  30653  icccncfext  31045  itgsin0pilem1  31086  stoweidlem13  31132  wallispilem2  31185  wallispilem4  31187  wallispi2lem1  31190  stirlinglem13  31205  dirkertrigeqlem3  31219  dirkeritg  31221  fourierdlem42  31268  fourierdlem62  31288  fourierdlem102  31328  fourierdlem103  31329  fourierdlem104  31330  fourierdlem114  31340  sqwvfoura  31348  fourierswlem  31350  fouriersw  31351  usg2spot2nb  31784  zlmodzxz0  31884  zlmodzxzequa  32053  zlmodzxzequap  32056  zlmodzxzldeplem3  32059  ax6e2ndeqALT  32686  sineq0ALT  32692  bj-pirp  33555  bj-minftyccb  33575  dihjatcclem4  36093  pirp  36640  taupilem2  36643
  Copyright terms: Public domain W3C validator