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

Theorem mp3an 1326
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 1313 . 2  |-  ( ( ps  /\  ch )  ->  th )
61, 2, 5mp2an 670 1  |-  th
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 974
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 369  df-3an 976
This theorem is referenced by:  vtocl3  3113  raltp  4027  rextp  4028  funopg  5601  ftp  6062  caovass  6456  caovdi  6475  ordom  6692  ofmres  6780  omopthlem1  7341  omopthlem2  7342  omopthi  7343  xpcomen  7646  unfilem3  7820  hartogs  8003  card2on  8014  unwf  8260  tskwe  8363  alephsmo  8515  dfac4  8535  dfac2a  8542  ackbij1lem5  8636  ackbij1lem13  8644  axdc2lem  8860  axcclem  8869  ondomon  8970  cfpwsdom  8991  pwfseqlem2  9067  pwfseqlem3  9068  1lt2pi  9313  addassi  9634  mulassi  9635  adddii  9636  adddiri  9637  lttri  9742  lelttri  9743  ltletri  9744  letri  9745  ltadd2i  9747  ltadd2iOLD  9748  mul02lem2  9791  addid1  9794  addcani  9807  addcan2i  9808  mul12i  9809  mul32i  9810  add12i  9832  add32i  9833  subaddi  9943  subadd2i  9944  subsub23i  9946  addsubassi  9947  addsubi  9948  subcani  9949  subcan2i  9950  pnncani  9951  subdii  10046  subdiri  10047  ltadd1i  10147  leadd1i  10148  leadd2i  10149  ltsubaddi  10150  lesubaddi  10151  ltsubadd2i  10152  lesubadd2i  10153  ltaddsubi  10154  mulcani  10229  div23i  10343  div11i  10344  1mhlfehlf  10799  halfpm6th  10801  addex  11263  mulex  11264  unirnioo  11678  ioorebas  11680  uzenom  12116  nnenom  12131  m1expcl2  12232  i4  12315  expnass  12318  faclbnd4lem1  12415  bcn1  12435  ccatfnOLD  12645  cats1fvn  12879  cats1fv  12880  cats1cat  12882  abs3difi  13390  0.999...  13842  geoihalfsum  13843  bpoly3  14003  ef01bndlem  14128  cos1bnd  14131  cos2bnd  14132  sin4lt0  14139  rpnnen2lem3  14159  rpnnen2lem11  14167  rpnnen  14169  rexpen  14170  aleph1irr  14188  divalglem2  14262  ndvdsi  14277  gcdaddmlem  14375  bezout  14389  3prm  14443  dec2dvds  14758  modxai  14763  modsubi  14767  gcdi  14768  numexp2x  14774  prdsval  15069  prdsds  15078  mreexexd  15262  plusffval  16201  pmtrprfval  16836  m1expaddsub  16847  0frgp  17121  staffval  17816  scaffval  17850  cnfldcj  18747  cnfldds  18750  xrsadd  18755  xrsmul  18756  xrsds  18781  nn0srg  18806  rge0srg  18807  zring0  18818  cnmsgnsubg  18911  psgninv  18916  re0g  18946  ipffval  18981  ocvfval  18995  frlmbas  19084  frlmbasOLD  19085  mdetrlin  19396  mdetunilem9  19414  leordtval2  20006  iscnp2  20033  utop3cls  21046  nmfval  21401  nmoffn  21510  nmofval  21513  icccld  21566  addcnlem  21660  iimulcn  21730  icopnfhmeo  21735  iccpnfcnv  21736  iccpnfhmeo  21737  xrhmeo  21738  xrhmph  21739  oprpiece1res1  21743  oprpiece1res2  21744  ishtpy  21764  pcoass  21816  tchex  21952  cnfldcusp  22089  resscdrg  22090  reust  22105  recusp  22106  vitalilem4  22312  vitalilem5  22313  mbfdm  22327  dveflem  22672  dvlipcn  22687  c1lip2  22691  dgrid  22953  iaa  23013  abelthlem3  23120  abelthlem5  23122  abelth  23128  efcn  23130  sinhalfpilem  23148  sincosq1lem  23182  sincosq4sgn  23186  tangtx  23190  sincos4thpi  23198  sincos6thpi  23200  pige3  23202  relogcn  23313  dvlog2lem  23327  dvlog2  23328  logtayl  23335  logtayl2  23337  cxpsqrtlem  23377  cxpsqrt  23378  cxpcn2  23416  cxpcn3  23418  logblog  23459  ang180lem1  23468  ang180lem2  23469  1cubrlem  23497  mcubic  23503  quart1lem  23511  quart1  23512  reasinsin  23552  atancj  23566  efiatan  23568  atantan  23579  atanbndlem  23581  atan1  23584  atancn  23592  atantayl2  23594  log2cnv  23600  log2tlbnd  23601  log2ublem1  23602  log2ublem2  23603  log2ub  23605  efrlim  23625  scvxcvx  23641  1sgm2ppw  23856  ppiub  23860  bclbnd  23936  bposlem8  23947  lgsdir2lem1  23979  lgsdir2lem5  23983  lgseisenlem1  24005  lgseisenlem2  24006  lgsquadlem1  24010  chebbnd1  24038  dchrvmasumlem2  24064  istrkg3ld  24237  trgcgrg  24287  ax5seglem7  24655  axlowdimlem6  24667  axlowdimlem8  24669  axlowdimlem11  24672  cusgrasizeindb1  24888  3v3e3cycl1  25061  constr3lem2  25063  constr3lem5  25065  constr3trllem5  25071  erclwwlktr  25232  erclwwlkntr  25244  0egra0rgra  25353  vdegp1ai  25401  usg2spot2nb  25482  ex-fl  25585  0vfval  25913  smcnlem  26021  lnocoi  26086  nmlno0lem  26122  nmblolbii  26128  blocnilem  26133  blocni  26134  cncph  26148  isph  26151  ip0i  26154  ip1ilem  26155  ip2i  26157  ipdirilem  26158  ipasslem7  26165  ipasslem8  26166  ipasslem9  26167  ipasslem10  26168  ipasslem11  26169  ip2dii  26173  pythi  26179  siilem1  26180  siilem2  26181  siii  26182  hvmulassi  26377  hvmulcomi  26378  hvdistr1i  26382  hvsubdistr1i  26383  hvassi  26384  hvadd32i  26385  hvsubassi  26386  hvsub32i  26387  normlem0  26440  normlem8  26448  normlem9  26449  bcseqi  26451  polid2i  26488  hhph  26509  hlim0  26567  shscli  26649  shlessi  26709  shlej1i  26710  omlsilem  26734  shlubi  26747  h1de2i  26885  pjadjii  27006  pjaddii  27007  pjmulii  27009  pjdifnormii  27015  pjcji  27016  hoaddsubassi  27152  eigrei  27166  eigposi  27168  eigorthi  27169  adj0  27326  lnopeq0lem1  27337  lnopunilem1  27342  lnophmlem2  27349  nmcexi  27358  nmcopexi  27359  lnfn0i  27374  nmcfnexi  27383  mdexchi  27667  xppreima2  27931  elxrge02  28080  xrge0adddir  28134  xrnarchi  28180  xrge0slmod  28287  raddcn  28364  xrge0iifcnv  28368  xrge0iifiso  28370  xrge0iifhmeo  28371  xrge0iifhom  28372  xrge0iifmhm  28374  xrge0mulc1cn  28376  lmlimxrge0  28383  pnfneige0  28386  lmxrge0  28387  zringnm  28393  rezh  28404  qqh0  28417  qqh1  28418  qqhucn  28425  esumpinfval  28520  hashf2  28531  esumcvg  28533  br2base  28717  sxbrsigalem3  28720  dya2iocbrsiga  28723  dya2icobrsiga  28724  sxbrsigalem1  28733  sxbrsigalem2  28734  sxbrsigalem4  28735  sxbrsigalem5  28736  sxbrsiga  28738  oms0  28745  ballotlem2  28933  ballotlem4  28943  ballotlemi1  28947  ballotth  28982  sgnclre  28984  signstf  29029  subfacp1lem1  29476  subfacp1lem6  29482  kur14lem6  29508  cvmliftlem4  29585  problem4  29874  quad3  29876  logi  29943  iexpire  29944  fununiq  29983  fvtransport  30370  bj-minftyccb  31192  taupilem2  31248  cos2h  31418  tan2h  31419  ismblfin  31427  mbfposadd  31434  ftc1anclem5  31467  asindmre  31473  dvasin  31474  dvacos  31475  rrnval  31605  dihjatcclem4  34441  rabren3dioph  35110  jm2.27dlem2  35314  rmydioph  35318  rmxdioph  35320  expdiophlem2  35326  expdioph  35327  arearect  35547  areaquad  35548  corclrcl  35686  iunrelexpuztr  35698  corcltrcl  35718  dffrege76  35920  lhe4.4ex1a  36082  binomcxplemdvbinom  36106  binomcxplemnotnn0  36109  ax6e2ndeqALT  36762  sineq0ALT  36768  lptioo2cn  37019  icccncfext  37058  itgsin0pilem1  37116  itgsbtaddcnst  37149  stoweidlem13  37163  wallispilem2  37216  wallispilem4  37218  wallispi2lem1  37221  stirlinglem13  37236  dirkerper  37246  dirkertrigeqlem3  37250  dirkeritg  37252  dirkercncflem1  37253  dirkercncflem4  37256  fourierdlem42  37299  fourierdlem62  37319  fourierdlem102  37359  fourierdlem103  37360  fourierdlem104  37361  fourierdlem114  37371  sqwvfoura  37379  fourierswlem  37381  fouriersw  37382  6gbe  37825  7gbo  37826  8gbe  37827  9gboa  37828  11gboa  37829  sgoldbalt  37835  nnsum4primesevenALTV  37849  3exp4mod41  37862  41prothprmlem2  37864  0nodd  38127  oddinmgm  38132  2zrng0  38255  zlmodzxz0  38456  zlmodzxzequa  38608  zlmodzxzequap  38611  zlmodzxzldeplem3  38614  3halfnz  38637  nnlog2ge0lt1  38697  blen1  38715  blen2  38716  nnolog2flm1  38721
  Copyright terms: Public domain W3C validator