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

Theorem mp3an 1578
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 1565 . 2 ((𝜓𝜒) → 𝜃)
61, 2, 5mp2an 675 1 𝜃
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  vtocl3  3466  raltp  4443  rextp  4444  opthhausdorff  5185  funopg  6145  feq12i  6259  ftp  6658  caovass  7074  caovdi  7093  ordom  7314  ofmres  7404  omopthlem1  7982  omopthlem2  7983  omopthi  7984  xpcomen  8300  unfilem3  8475  hartogs  8698  card2on  8708  unwf  8930  inlresf1  9034  inrresf1  9036  tskwe  9069  alephsmo  9218  dfac4  9238  dfac2a  9245  ackbij1lem13  9349  axdc2lem  9565  axcclem  9574  ondomon  9680  cfpwsdom  9701  pwfseqlem2  9776  pwfseqlem3  9777  1lt2pi  10022  addassi  10345  mulassi  10346  adddii  10347  adddiri  10348  lttri  10458  lelttri  10459  ltletri  10460  letri  10461  ltadd2i  10463  mul02lem2  10508  addid1  10511  addcani  10524  addcan2i  10525  mul12i  10526  mul32i  10527  add12i  10553  add32i  10554  subaddi  10663  subadd2i  10664  subsub23i  10666  addsubassi  10667  addsubi  10668  subcani  10669  subcan2i  10670  pnncani  10671  subdii  10774  subdiri  10775  ltadd1i  10877  leadd1i  10878  leadd2i  10879  ltsubaddi  10880  lesubaddi  10881  ltsubadd2i  10882  lesubadd2i  10883  ltaddsubi  10884  mulcani  10961  div23i  11078  div11i  11079  1mhlfehlf  11538  halfpm6th  11540  3halfnz  11742  addex  12064  mulex  12065  unirnioo  12512  ioorebas  12514  xnn0xrge0  12568  fldiv4lem1div2  12882  uzenom  13007  nnenom  13023  m1expcl2  13125  i4  13210  expnass  13213  faclbnd4lem1  13320  bcn1  13340  hashfxnn0  13364  cats1fvn  13847  cats1fv  13848  cats1cat  13850  cats2cat  13851  wrdlen3s3  13937  abs3difi  14391  0.999...  14854  bpoly3  15029  ef01bndlem  15154  cos1bnd  15157  cos2bnd  15158  sin4lt0  15165  rpnnen2lem3  15185  rpnnen2lem11  15193  rpnnen  15196  rexpen  15197  aleph1irr  15215  3dvdsdec  15296  3dvds2dec  15297  divalglem2  15358  ndvdsi  15375  flodddiv4  15376  gcdaddmlem  15484  bezout  15499  3lcm2e6woprm  15567  6lcm4e12  15568  lcmf0  15586  lcmf2a3a4e12  15599  3prm  15644  dec2dvds  16004  modxai  16009  modsubi  16013  gcdi  16014  numexp2x  16020  prdsval  16340  prdsds  16349  plusffval  17472  pmtrprfval  18128  m1expaddsub  18139  0frgp  18413  staffval  19071  scaffval  19105  cnfldcj  19981  cnfldds  19984  cnfldfun  19986  xrsadd  19991  xrsmul  19992  xrsds  20017  cnmgpid  20036  nn0srg  20044  rge0srg  20045  zring0  20056  cnmsgnsubg  20150  psgninv  20155  re0g  20187  ipffval  20223  ocvfval  20241  frlmbas  20330  mdetrlin  20640  mdetunilem9  20658  leordtval2  21251  iscnp2  21278  utop3cls  22289  nmfval  22627  nmoffn  22749  nmofval  22752  icccld  22804  addcnlem  22901  iimulcn  22971  icopnfhmeo  22976  iccpnfcnv  22977  iccpnfhmeo  22978  xrhmeo  22979  xrhmph  22980  oprpiece1res1  22984  oprpiece1res2  22985  ishtpy  23005  pcoass  23057  cnstrcvs  23174  cncvs  23178  recvs  23179  qcvs  23180  zclmncvs  23181  tchex  23249  cnfldcusp  23387  resscdrg  23388  reust  23404  recusp  23405  vitalilem4  23615  vitalilem5  23616  mbfdm  23630  dveflem  23979  dvlipcn  23994  c1lip2  23998  dgrid  24257  iaa  24317  abelthlem3  24424  abelthlem5  24426  abelth  24432  efcn  24434  sinhalfpilem  24453  sincosq1lem  24487  sincosq4sgn  24491  tangtx  24495  sincos4thpi  24503  sincos6thpi  24505  pige3  24507  relogcn  24621  dvlog2lem  24635  dvlog2  24636  logtayl  24643  logtayl2  24645  cxpsqrtlem  24685  cxpsqrt  24686  cxpcn2  24724  cxpcn3  24726  logblog  24767  ang180lem1  24776  ang180lem2  24777  1cubrlem  24805  mcubic  24811  quart1lem  24819  quart1  24820  reasinsin  24860  atancj  24874  efiatan  24876  atantan  24887  atanbndlem  24889  atan1  24892  atancn  24900  atantayl2  24902  log2cnv  24908  log2tlbnd  24909  log2ublem1  24910  log2ublem2  24911  log2ub  24913  efrlim  24933  scvxcvx  24949  1sgm2ppw  25162  ppiub  25166  bclbnd  25242  bposlem8  25253  lgsdir2lem1  25287  lgsdir2lem5  25291  lgseisenlem1  25337  lgseisenlem2  25338  lgsquadlem1  25342  chebbnd1  25398  dchrvmasumlem2  25424  istrkg3ld  25597  trgcgrg  25647  ax5seglem7  26052  axlowdimlem6  26064  axlowdimlem8  26066  axlowdimlem11  26069  cusgrsizeindb1  26597  vtxdginducedm1  26690  0grrusgr  26726  erclwwlktr  27188  erclwwlkntr  27245  wlk2v2e  27353  upgr3v3e3cycl  27376  konigsberglem1  27448  konigsberglem2  27449  konigsberglem3  27450  konigsberglem5  27452  ex-fl  27658  ex-mod  27660  ex-hash  27664  ex-lcm  27669  0vfval  27812  smcnlem  27903  lnocoi  27963  nmlno0lem  27999  nmblolbii  28005  blocnilem  28010  blocni  28011  cncph  28025  isph  28028  ip0i  28031  ip1ilem  28032  ip2i  28034  ipdirilem  28035  ipasslem7  28042  ipasslem8  28043  ipasslem9  28044  ipasslem10  28045  ipasslem11  28046  ip2dii  28050  pythi  28056  siilem1  28057  siilem2  28058  siii  28059  hvmulassi  28254  hvmulcomi  28255  hvdistr1i  28259  hvsubdistr1i  28260  hvassi  28261  hvadd32i  28262  hvsubassi  28263  hvsub32i  28264  normlem0  28317  normlem8  28325  normlem9  28326  bcseqi  28328  polid2i  28365  hhph  28386  hlim0  28443  shscli  28527  shlessi  28587  shlej1i  28588  omlsilem  28612  shlubi  28625  h1de2i  28763  pjadjii  28884  pjaddii  28885  pjmulii  28887  pjdifnormii  28893  pjcji  28894  hoaddsubassi  29030  eigrei  29044  eigposi  29046  eigorthi  29047  adj0  29204  lnopeq0lem1  29215  lnopunilem1  29220  lnophmlem2  29227  nmcexi  29236  nmcopexi  29237  lnfn0i  29252  nmcfnexi  29261  mdexchi  29545  xppreima2  29800  dp2clq  29937  dp2lt  29941  dp2ltc  29943  dpexpp1  29964  dpmul  29969  dpmul4  29970  elxrge02  29988  xrge0adddir  30040  xrnarchi  30086  xrge0slmod  30192  psgnid  30195  raddcn  30323  xrge0iifcnv  30327  xrge0iifiso  30329  xrge0iifhmeo  30330  xrge0iifhom  30331  xrge0iifmhm  30333  xrge0mulc1cn  30335  lmlimxrge0  30342  pnfneige0  30345  lmxrge0  30346  zringnm  30352  rezh  30363  qqh0  30376  qqh1  30377  qqhucn  30384  esumpinfval  30483  hashf2  30494  esumcvg  30496  br2base  30679  sxbrsigalem3  30682  dya2iocbrsiga  30685  dya2icobrsiga  30686  sxbrsigalem1  30695  sxbrsigalem2  30696  sxbrsigalem4  30697  sxbrsigalem5  30698  sxbrsiga  30700  ballotlem2  30898  ballotlem4  30908  ballotlemi1  30912  ballotth  30947  sgnclre  30949  signstf  30991  itgexpif  31032  chtvalz  31055  hgt750lemd  31074  hgt750lem  31077  tgoldbachgnn  31085  subfacp1lem1  31506  subfacp1lem6  31512  kur14lem6  31538  cvmliftlem4  31615  problem4  31906  quad3  31908  logi  31964  iexpire  31965  fununiq  32011  fvtransport  32482  bj-minftyccb  33448  taupilem2  33504  1oequni2o  33551  finxp1o  33564  finxpreclem4  33566  cos2h  33732  tan2h  33733  pigt3  33734  poimirlem9  33750  poimirlem27  33768  poimirlem28  33769  ismblfin  33782  mbfposadd  33788  ftc1anclem5  33820  asindmre  33826  dvasin  33827  dvacos  33828  rrnval  33956  el3v  34327  dihjatcclem4  37220  rabren3dioph  37899  jm2.27dlem2  38096  rmydioph  38100  rmxdioph  38102  expdiophlem2  38108  expdioph  38109  arearect  38319  areaquad  38320  corclrcl  38517  iunrelexpuztr  38529  corcltrcl  38549  dffrege76  38751  k0004val0  38970  lhe4.4ex1a  39046  binomcxplemdvbinom  39070  binomcxplemnotnn0  39073  ax6e2ndeqALT  39679  sineq0ALT  39685  pnfel0pnf  40253  lptioo2cn  40375  limsup10ex  40503  liminf10ex  40504  icccncfext  40598  itgsin0pilem1  40663  itgsbtaddcnst  40695  stoweidlem13  40727  wallispilem2  40780  wallispilem4  40782  wallispi2lem1  40785  stirlinglem13  40800  dirkerper  40810  dirkertrigeqlem3  40814  dirkeritg  40816  dirkercncflem1  40817  dirkercncflem4  40820  fourierdlem42  40863  fourierdlem62  40882  fourierdlem102  40922  fourierdlem103  40923  fourierdlem104  40924  fourierdlem114  40934  sqwvfoura  40942  fourierswlem  40944  fouriersw  40945  smfmullem4  41501  fmtnoprmfac2lem1  42071  fmtno4prm  42080  2exp5  42100  2exp11  42110  3exp4mod41  42126  41prothprmlem2  42128  6gbe  42252  7gbow  42253  8gbe  42254  9gbo  42255  11gbo  42256  sbgoldbalt  42262  nnsum4primesevenALTV  42282  0nodd  42396  oddinmgm  42401  2zrng0  42524  zlmodzxz0  42720  zlmodzxzequa  42871  zlmodzxzequap  42874  zlmodzxzldeplem3  42877  nnlog2ge0lt1  42946  blen1  42964  blen2  42965  nnolog2flm1  42970
  Copyright terms: Public domain W3C validator