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

Theorem mp3an 1415
Description: An inference based on modus ponens. (Contributed by NM, 14-May-1999.)
Hypotheses
Ref Expression
mp3an.1 𝜑
mp3an.2 𝜓
mp3an.3 𝜒
mp3an.4 ((𝜑𝜓𝜒) → 𝜃)
Assertion
Ref Expression
mp3an 𝜃

Proof of Theorem mp3an
StepHypRef Expression
1 mp3an.2 . 2 𝜓
2 mp3an.3 . 2 𝜒
3 mp3an.1 . . 3 𝜑
4 mp3an.4 . . 3 ((𝜑𝜓𝜒) → 𝜃)
53, 4mp3an1 1402 . 2 ((𝜓𝜒) → 𝜃)
61, 2, 5mp2an 703 1 𝜃
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  vtocl3  3234  raltp  4186  rextp  4187  funopg  5822  feq12i  5937  ftp  6307  caovass  6709  caovdi  6728  ordom  6943  ofmres  7032  omopthlem1  7599  omopthlem2  7600  omopthi  7601  xpcomen  7913  unfilem3  8088  hartogs  8309  card2on  8319  unwf  8533  tskwe  8636  alephsmo  8785  dfac4  8805  dfac2a  8812  ackbij1lem5  8906  ackbij1lem13  8914  axdc2lem  9130  axcclem  9139  ondomon  9241  cfpwsdom  9262  pwfseqlem2  9337  pwfseqlem3  9338  1lt2pi  9583  addassi  9904  mulassi  9905  adddii  9906  adddiri  9907  lttri  10014  lelttri  10015  ltletri  10016  letri  10017  ltadd2i  10019  mul02lem2  10064  addid1  10067  addcani  10080  addcan2i  10081  mul12i  10082  mul32i  10083  add12i  10109  add32i  10110  subaddi  10219  subadd2i  10220  subsub23i  10222  addsubassi  10223  addsubi  10224  subcani  10225  subcan2i  10226  pnncani  10227  subdii  10329  subdiri  10330  ltadd1i  10431  leadd1i  10432  leadd2i  10433  ltsubaddi  10434  lesubaddi  10435  ltsubadd2i  10436  lesubadd2i  10437  ltaddsubi  10438  mulcani  10515  div23i  10632  div11i  10633  1mhlfehlf  11098  halfpm6th  11100  3halfnz  11288  addex  11662  mulex  11663  unirnioo  12100  ioorebas  12102  fldiv4lem1div2  12455  uzenom  12580  nnenom  12596  m1expcl2  12699  i4  12784  expnass  12787  faclbnd4lem1  12897  bcn1  12917  cats1fvn  13400  cats1fv  13401  cats1cat  13403  cats2cat  13404  wrdlen3s3  13486  abs3difi  13942  0.999...  14397  0.999...OLD  14398  geoihalfsum  14399  bpoly3  14574  ef01bndlem  14699  cos1bnd  14702  cos2bnd  14703  sin4lt0  14710  rpnnen2lem3  14730  rpnnen2lem11  14738  rpnnen  14741  rexpen  14742  aleph1irr  14760  3dvdsdec  14838  3dvdsdecOLD  14839  3dvds2dec  14840  3dvds2decOLD  14841  divalglem2  14902  ndvdsi  14920  flodddiv4  14921  gcdaddmlem  15029  bezout  15044  3lcm2e6woprm  15112  6lcm4e12  15113  lcmf0  15131  lcmf2a3a4e12  15144  3prm  15190  dec2dvds  15551  modxai  15556  modsubi  15560  gcdi  15561  numexp2x  15567  prdsval  15884  prdsds  15893  mreexexdOLD  16078  plusffval  17016  pmtrprfval  17676  m1expaddsub  17687  0frgp  17961  staffval  18616  scaffval  18650  cnfldcj  19520  cnfldds  19523  xrsadd  19528  xrsmul  19529  xrsds  19554  cnmgpid  19573  nn0srg  19581  rge0srg  19582  zring0  19593  cnmsgnsubg  19687  psgninv  19692  re0g  19722  ipffval  19757  ocvfval  19771  frlmbas  19860  mdetrlin  20169  mdetunilem9  20187  leordtval2  20768  iscnp2  20795  utop3cls  21807  nmfval  22144  nmoffn  22257  nmofval  22260  icccld  22312  addcnlem  22406  iimulcn  22476  icopnfhmeo  22481  iccpnfcnv  22482  iccpnfhmeo  22483  xrhmeo  22484  xrhmph  22485  oprpiece1res1  22489  oprpiece1res2  22490  ishtpy  22510  pcoass  22563  cnstrcvs  22678  cncvs  22682  tchex  22745  cnfldcusp  22878  resscdrg  22879  reust  22894  recusp  22895  vitalilem4  23103  vitalilem5  23104  mbfdm  23118  dveflem  23463  dvlipcn  23478  c1lip2  23482  dgrid  23741  iaa  23801  abelthlem3  23908  abelthlem5  23910  abelth  23916  efcn  23918  sinhalfpilem  23936  sincosq1lem  23970  sincosq4sgn  23974  tangtx  23978  sincos4thpi  23986  sincos6thpi  23988  pige3  23990  relogcn  24101  dvlog2lem  24115  dvlog2  24116  logtayl  24123  logtayl2  24125  cxpsqrtlem  24165  cxpsqrt  24166  cxpcn2  24204  cxpcn3  24206  logblog  24247  ang180lem1  24256  ang180lem2  24257  1cubrlem  24285  mcubic  24291  quart1lem  24299  quart1  24300  reasinsin  24340  atancj  24354  efiatan  24356  atantan  24367  atanbndlem  24369  atan1  24372  atancn  24380  atantayl2  24382  log2cnv  24388  log2tlbnd  24389  log2ublem1  24390  log2ublem2  24391  log2ub  24393  efrlim  24413  scvxcvx  24429  1sgm2ppw  24642  ppiub  24646  bclbnd  24722  bposlem8  24733  lgsdir2lem1  24767  lgsdir2lem5  24771  lgseisenlem1  24817  lgseisenlem2  24818  lgsquadlem1  24822  chebbnd1  24878  dchrvmasumlem2  24904  istrkg3ld  25077  trgcgrg  25128  ax5seglem7  25533  axlowdimlem6  25545  axlowdimlem8  25547  axlowdimlem11  25550  cusgrasizeindb1  25766  3v3e3cycl1  25938  constr3lem2  25940  constr3lem5  25942  constr3trllem5  25948  erclwwlktr  26109  erclwwlkntr  26121  0egra0rgra  26229  vdegp1ai  26277  usg2spot2nb  26358  ex-fl  26462  ex-mod  26464  ex-hash  26468  ex-lcm  26473  0vfval  26629  smcnlem  26737  lnocoi  26802  nmlno0lem  26838  nmblolbii  26844  blocnilem  26849  blocni  26850  cncph  26864  isph  26867  ip0i  26870  ip1ilem  26871  ip2i  26873  ipdirilem  26874  ipasslem7  26881  ipasslem8  26882  ipasslem9  26883  ipasslem10  26884  ipasslem11  26885  ip2dii  26889  pythi  26895  siilem1  26896  siilem2  26897  siii  26898  hvmulassi  27093  hvmulcomi  27094  hvdistr1i  27098  hvsubdistr1i  27099  hvassi  27100  hvadd32i  27101  hvsubassi  27102  hvsub32i  27103  normlem0  27156  normlem8  27164  normlem9  27165  bcseqi  27167  polid2i  27204  hhph  27225  hlim0  27282  shscli  27366  shlessi  27426  shlej1i  27427  omlsilem  27451  shlubi  27464  h1de2i  27602  pjadjii  27723  pjaddii  27724  pjmulii  27726  pjdifnormii  27732  pjcji  27733  hoaddsubassi  27869  eigrei  27883  eigposi  27885  eigorthi  27886  adj0  28043  lnopeq0lem1  28054  lnopunilem1  28059  lnophmlem2  28066  nmcexi  28075  nmcopexi  28076  lnfn0i  28091  nmcfnexi  28100  mdexchi  28384  xppreima2  28636  elxrge02  28777  xrge0adddir  28829  xrnarchi  28875  xrge0slmod  28981  psgnid  28984  raddcn  29109  xrge0iifcnv  29113  xrge0iifiso  29115  xrge0iifhmeo  29116  xrge0iifhom  29117  xrge0iifmhm  29119  xrge0mulc1cn  29121  lmlimxrge0  29128  pnfneige0  29131  lmxrge0  29132  zringnm  29138  rezh  29149  qqh0  29162  qqh1  29163  qqhucn  29170  esumpinfval  29268  hashf2  29279  esumcvg  29281  br2base  29464  sxbrsigalem3  29467  dya2iocbrsiga  29470  dya2icobrsiga  29471  sxbrsigalem1  29480  sxbrsigalem2  29481  sxbrsigalem4  29482  sxbrsigalem5  29483  sxbrsiga  29485  ballotlem2  29683  ballotlem4  29693  ballotlemi1  29697  ballotth  29732  sgnclre  29734  signstf  29775  subfacp1lem1  30221  subfacp1lem6  30227  kur14lem6  30253  cvmliftlem4  30330  problem4  30622  quad3  30624  logi  30679  iexpire  30680  fununiq  30719  fvtransport  31115  bj-minftyccb  32085  taupilem2  32141  1oequni2o  32188  finxp1o  32201  finxpreclem4  32203  cos2h  32366  tan2h  32367  pigt3  32368  poimirlem9  32384  poimirlem27  32402  poimirlem28  32403  ismblfin  32416  mbfposadd  32423  ftc1anclem5  32455  asindmre  32461  dvasin  32462  dvacos  32463  rrnval  32592  dihjatcclem4  35524  rabren3dioph  36193  jm2.27dlem2  36391  rmydioph  36395  rmxdioph  36397  expdiophlem2  36403  expdioph  36404  arearect  36616  areaquad  36617  corclrcl  36814  iunrelexpuztr  36826  corcltrcl  36846  dffrege76  37049  k0004val0  37268  lhe4.4ex1a  37346  binomcxplemdvbinom  37370  binomcxplemnotnn0  37373  ax6e2ndeqALT  37985  sineq0ALT  37991  pnfel0pnf  38398  lptioo2cn  38509  icccncfext  38570  itgsin0pilem1  38638  itgsbtaddcnst  38671  stoweidlem13  38703  wallispilem2  38756  wallispilem4  38758  wallispi2lem1  38761  stirlinglem13  38776  dirkerper  38786  dirkertrigeqlem3  38790  dirkeritg  38792  dirkercncflem1  38793  dirkercncflem4  38796  fourierdlem42  38839  fourierdlem62  38858  fourierdlem102  38898  fourierdlem103  38899  fourierdlem104  38900  fourierdlem114  38910  sqwvfoura  38918  fourierswlem  38920  fouriersw  38921  smfmullem4  39476  fmtnoprmfac2lem1  39814  fmtno4prm  39823  2exp5  39843  2exp11  39853  3exp4mod41  39869  41prothprmlem2  39871  6gbe  39991  7gbo  39992  8gbe  39993  9gboa  39994  11gboa  39995  sgoldbalt  40001  nnsum4primesevenALTV  40015  xnn0xrge0  40198  cusgrsizeindb1  40661  0grrusgr  40774  erclwwlkstr  41238  erclwwlksntr  41250  1wlk2v2e  41319  ntrl2v2e  41320  upgr3v3e3cycl  41342  konigsberglem1  41417  konigsberglem2  41418  konigsberglem3  41419  konigsberglem5  41421  0nodd  41595  oddinmgm  41600  2zrng0  41723  zlmodzxz0  41922  zlmodzxzequa  42074  zlmodzxzequap  42077  zlmodzxzldeplem3  42080  nnlog2ge0lt1  42153  blen1  42171  blen2  42172  nnolog2flm1  42177
  Copyright terms: Public domain W3C validator