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

Theorem mp3an 1416
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 1403 . 2 ((𝜓𝜒) → 𝜃)
61, 2, 5mp2an 704 1 𝜃
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1031
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 196  df-an 385  df-3an 1033
This theorem is referenced by:  vtocl3  3235  raltp  4187  rextp  4188  funopg  5836  feq12i  5951  ftp  6329  caovass  6732  caovdi  6751  ordom  6966  ofmres  7055  omopthlem1  7622  omopthlem2  7623  omopthi  7624  xpcomen  7936  unfilem3  8111  hartogs  8332  card2on  8342  unwf  8556  tskwe  8659  alephsmo  8808  dfac4  8828  dfac2a  8835  ackbij1lem5  8929  ackbij1lem13  8937  axdc2lem  9153  axcclem  9162  ondomon  9264  cfpwsdom  9285  pwfseqlem2  9360  pwfseqlem3  9361  1lt2pi  9606  addassi  9927  mulassi  9928  adddii  9929  adddiri  9930  lttri  10042  lelttri  10043  ltletri  10044  letri  10045  ltadd2i  10047  mul02lem2  10092  addid1  10095  addcani  10108  addcan2i  10109  mul12i  10110  mul32i  10111  add12i  10137  add32i  10138  subaddi  10247  subadd2i  10248  subsub23i  10250  addsubassi  10251  addsubi  10252  subcani  10253  subcan2i  10254  pnncani  10255  subdii  10358  subdiri  10359  ltadd1i  10461  leadd1i  10462  leadd2i  10463  ltsubaddi  10464  lesubaddi  10465  ltsubadd2i  10466  lesubadd2i  10467  ltaddsubi  10468  mulcani  10545  div23i  10662  div11i  10663  1mhlfehlf  11128  halfpm6th  11130  3halfnz  11332  addex  11706  mulex  11707  unirnioo  12144  ioorebas  12146  xnn0xrge0  12196  fldiv4lem1div2  12500  uzenom  12625  nnenom  12641  m1expcl2  12744  i4  12829  expnass  12832  faclbnd4lem1  12942  bcn1  12962  hashfxnn0  12986  cats1fvn  13454  cats1fv  13455  cats1cat  13457  cats2cat  13458  wrdlen3s3  13540  abs3difi  13996  0.999...  14451  0.999...OLD  14452  geoihalfsum  14453  bpoly3  14628  ef01bndlem  14753  cos1bnd  14756  cos2bnd  14757  sin4lt0  14764  rpnnen2lem3  14784  rpnnen2lem11  14792  rpnnen  14795  rexpen  14796  aleph1irr  14814  3dvdsdec  14892  3dvdsdecOLD  14893  3dvds2dec  14894  3dvds2decOLD  14895  divalglem2  14956  ndvdsi  14974  flodddiv4  14975  gcdaddmlem  15083  bezout  15098  3lcm2e6woprm  15166  6lcm4e12  15167  lcmf0  15185  lcmf2a3a4e12  15198  3prm  15244  dec2dvds  15605  modxai  15610  modsubi  15614  gcdi  15615  numexp2x  15621  prdsval  15938  prdsds  15947  mreexexdOLD  16132  plusffval  17070  pmtrprfval  17730  m1expaddsub  17741  0frgp  18015  staffval  18670  scaffval  18704  cnfldcj  19574  cnfldds  19577  xrsadd  19582  xrsmul  19583  xrsds  19608  cnmgpid  19627  nn0srg  19635  rge0srg  19636  zring0  19647  cnmsgnsubg  19742  psgninv  19747  re0g  19777  ipffval  19812  ocvfval  19829  frlmbas  19918  mdetrlin  20227  mdetunilem9  20245  leordtval2  20826  iscnp2  20853  utop3cls  21865  nmfval  22203  nmoffn  22325  nmofval  22328  icccld  22380  addcnlem  22475  iimulcn  22545  icopnfhmeo  22550  iccpnfcnv  22551  iccpnfhmeo  22552  xrhmeo  22553  xrhmph  22554  oprpiece1res1  22558  oprpiece1res2  22559  ishtpy  22579  pcoass  22632  cnstrcvs  22749  cncvs  22753  recvs  22754  qcvs  22755  zclmncvs  22756  tchex  22824  cnfldcusp  22961  resscdrg  22962  reust  22977  recusp  22978  vitalilem4  23186  vitalilem5  23187  mbfdm  23201  dveflem  23546  dvlipcn  23561  c1lip2  23565  dgrid  23824  iaa  23884  abelthlem3  23991  abelthlem5  23993  abelth  23999  efcn  24001  sinhalfpilem  24019  sincosq1lem  24053  sincosq4sgn  24057  tangtx  24061  sincos4thpi  24069  sincos6thpi  24071  pige3  24073  relogcn  24184  dvlog2lem  24198  dvlog2  24199  logtayl  24206  logtayl2  24208  cxpsqrtlem  24248  cxpsqrt  24249  cxpcn2  24287  cxpcn3  24289  logblog  24330  ang180lem1  24339  ang180lem2  24340  1cubrlem  24368  mcubic  24374  quart1lem  24382  quart1  24383  reasinsin  24423  atancj  24437  efiatan  24439  atantan  24450  atanbndlem  24452  atan1  24455  atancn  24463  atantayl2  24465  log2cnv  24471  log2tlbnd  24472  log2ublem1  24473  log2ublem2  24474  log2ub  24476  efrlim  24496  scvxcvx  24512  1sgm2ppw  24725  ppiub  24729  bclbnd  24805  bposlem8  24816  lgsdir2lem1  24850  lgsdir2lem5  24854  lgseisenlem1  24900  lgseisenlem2  24901  lgsquadlem1  24905  chebbnd1  24961  dchrvmasumlem2  24987  istrkg3ld  25160  trgcgrg  25210  ax5seglem7  25615  axlowdimlem6  25627  axlowdimlem8  25629  axlowdimlem11  25632  cusgrasizeindb1  26000  3v3e3cycl1  26172  constr3lem2  26174  constr3lem5  26176  constr3trllem5  26182  erclwwlktr  26343  erclwwlkntr  26355  0egra0rgra  26463  vdegp1ai  26511  usg2spot2nb  26592  ex-fl  26696  ex-mod  26698  ex-hash  26702  ex-lcm  26707  0vfval  26845  smcnlem  26936  lnocoi  26996  nmlno0lem  27032  nmblolbii  27038  blocnilem  27043  blocni  27044  cncph  27058  isph  27061  ip0i  27064  ip1ilem  27065  ip2i  27067  ipdirilem  27068  ipasslem7  27075  ipasslem8  27076  ipasslem9  27077  ipasslem10  27078  ipasslem11  27079  ip2dii  27083  pythi  27089  siilem1  27090  siilem2  27091  siii  27092  hvmulassi  27287  hvmulcomi  27288  hvdistr1i  27292  hvsubdistr1i  27293  hvassi  27294  hvadd32i  27295  hvsubassi  27296  hvsub32i  27297  normlem0  27350  normlem8  27358  normlem9  27359  bcseqi  27361  polid2i  27398  hhph  27419  hlim0  27476  shscli  27560  shlessi  27620  shlej1i  27621  omlsilem  27645  shlubi  27658  h1de2i  27796  pjadjii  27917  pjaddii  27918  pjmulii  27920  pjdifnormii  27926  pjcji  27927  hoaddsubassi  28063  eigrei  28077  eigposi  28079  eigorthi  28080  adj0  28237  lnopeq0lem1  28248  lnopunilem1  28253  lnophmlem2  28260  nmcexi  28269  nmcopexi  28270  lnfn0i  28285  nmcfnexi  28294  mdexchi  28578  xppreima2  28830  elxrge02  28971  xrge0adddir  29023  xrnarchi  29069  xrge0slmod  29175  psgnid  29178  raddcn  29303  xrge0iifcnv  29307  xrge0iifiso  29309  xrge0iifhmeo  29310  xrge0iifhom  29311  xrge0iifmhm  29313  xrge0mulc1cn  29315  lmlimxrge0  29322  pnfneige0  29325  lmxrge0  29326  zringnm  29332  rezh  29343  qqh0  29356  qqh1  29357  qqhucn  29364  esumpinfval  29462  hashf2  29473  esumcvg  29475  br2base  29658  sxbrsigalem3  29661  dya2iocbrsiga  29664  dya2icobrsiga  29665  sxbrsigalem1  29674  sxbrsigalem2  29675  sxbrsigalem4  29676  sxbrsigalem5  29677  sxbrsiga  29679  ballotlem2  29877  ballotlem4  29887  ballotlemi1  29891  ballotth  29926  sgnclre  29928  signstf  29969  subfacp1lem1  30415  subfacp1lem6  30421  kur14lem6  30447  cvmliftlem4  30524  problem4  30816  quad3  30818  logi  30873  iexpire  30874  fununiq  30913  fvtransport  31309  bj-minftyccb  32289  taupilem2  32345  1oequni2o  32392  finxp1o  32405  finxpreclem4  32407  cos2h  32570  tan2h  32571  pigt3  32572  poimirlem9  32588  poimirlem27  32606  poimirlem28  32607  ismblfin  32620  mbfposadd  32627  ftc1anclem5  32659  asindmre  32665  dvasin  32666  dvacos  32667  rrnval  32796  dihjatcclem4  35728  rabren3dioph  36397  jm2.27dlem2  36595  rmydioph  36599  rmxdioph  36601  expdiophlem2  36607  expdioph  36608  arearect  36820  areaquad  36821  corclrcl  37018  iunrelexpuztr  37030  corcltrcl  37050  dffrege76  37253  k0004val0  37472  lhe4.4ex1a  37550  binomcxplemdvbinom  37574  binomcxplemnotnn0  37577  ax6e2ndeqALT  38189  sineq0ALT  38195  pnfel0pnf  38601  lptioo2cn  38712  icccncfext  38773  itgsin0pilem1  38841  itgsbtaddcnst  38874  stoweidlem13  38906  wallispilem2  38959  wallispilem4  38961  wallispi2lem1  38964  stirlinglem13  38979  dirkerper  38989  dirkertrigeqlem3  38993  dirkeritg  38995  dirkercncflem1  38996  dirkercncflem4  38999  fourierdlem42  39042  fourierdlem62  39061  fourierdlem102  39101  fourierdlem103  39102  fourierdlem104  39103  fourierdlem114  39113  sqwvfoura  39121  fourierswlem  39123  fouriersw  39124  smfmullem4  39679  fmtnoprmfac2lem1  40016  fmtno4prm  40025  2exp5  40045  2exp11  40055  3exp4mod41  40071  41prothprmlem2  40073  6gbe  40193  7gbo  40194  8gbe  40195  9gboa  40196  11gboa  40197  sgoldbalt  40203  nnsum4primesevenALTV  40217  cusgrsizeindb1  40666  0grrusgr  40779  erclwwlkstr  41243  erclwwlksntr  41255  1wlk2v2e  41324  ntrl2v2e  41325  upgr3v3e3cycl  41347  konigsberglem1  41422  konigsberglem2  41423  konigsberglem3  41424  konigsberglem5  41426  0nodd  41600  oddinmgm  41605  2zrng0  41728  zlmodzxz0  41927  zlmodzxzequa  42079  zlmodzxzequap  42082  zlmodzxzldeplem3  42085  nnlog2ge0lt1  42158  blen1  42176  blen2  42177  nnolog2flm1  42182
  Copyright terms: Public domain W3C validator