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

Theorem mp3an 1464
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 1451 . 2 ((𝜓𝜒) → 𝜃)
61, 2, 5mp2an 708 1 𝜃
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1054
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 197  df-an 385  df-3an 1056
This theorem is referenced by:  vtocl3  3293  raltp  4272  rextp  4273  funopg  5960  feq12i  6076  ftp  6464  caovass  6876  caovdi  6895  ordom  7116  ofmres  7206  omopthlem1  7780  omopthlem2  7781  omopthi  7782  xpcomen  8092  unfilem3  8267  hartogs  8490  card2on  8500  unwf  8711  tskwe  8814  alephsmo  8963  dfac4  8983  dfac2a  8990  ackbij1lem5  9084  ackbij1lem13  9092  axdc2lem  9308  axcclem  9317  ondomon  9423  cfpwsdom  9444  pwfseqlem2  9519  pwfseqlem3  9520  1lt2pi  9765  addassi  10086  mulassi  10087  adddii  10088  adddiri  10089  lttri  10201  lelttri  10202  ltletri  10203  letri  10204  ltadd2i  10206  mul02lem2  10251  addid1  10254  addcani  10267  addcan2i  10268  mul12i  10269  mul32i  10270  add12i  10296  add32i  10297  subaddi  10406  subadd2i  10407  subsub23i  10409  addsubassi  10410  addsubi  10411  subcani  10412  subcan2i  10413  pnncani  10414  subdii  10517  subdiri  10518  ltadd1i  10620  leadd1i  10621  leadd2i  10622  ltsubaddi  10623  lesubaddi  10624  ltsubadd2i  10625  lesubadd2i  10626  ltaddsubi  10627  mulcani  10704  div23i  10821  div11i  10822  1mhlfehlf  11289  halfpm6th  11291  3halfnz  11494  addex  11868  mulex  11869  unirnioo  12311  ioorebas  12313  xnn0xrge0  12363  fldiv4lem1div2  12678  uzenom  12803  nnenom  12819  m1expcl2  12922  i4  13007  expnass  13010  faclbnd4lem1  13120  bcn1  13140  hashfxnn0  13164  cats1fvn  13649  cats1fv  13650  cats1cat  13652  cats2cat  13653  wrdlen3s3  13738  abs3difi  14192  0.999...  14656  0.999...OLD  14657  geoihalfsum  14658  bpoly3  14833  ef01bndlem  14958  cos1bnd  14961  cos2bnd  14962  sin4lt0  14969  rpnnen2lem3  14989  rpnnen2lem11  14997  rpnnen  15000  rexpen  15001  aleph1irr  15019  3dvdsdec  15101  3dvdsdecOLD  15102  3dvds2dec  15103  3dvds2decOLD  15104  divalglem2  15165  ndvdsi  15183  flodddiv4  15184  gcdaddmlem  15292  bezout  15307  3lcm2e6woprm  15375  6lcm4e12  15376  lcmf0  15394  lcmf2a3a4e12  15407  3prm  15453  dec2dvds  15814  modxai  15819  modsubi  15823  gcdi  15824  numexp2x  15830  prdsval  16162  prdsds  16171  mreexexdOLD  16356  plusffval  17294  pmtrprfval  17953  m1expaddsub  17964  0frgp  18238  staffval  18895  scaffval  18929  cnfldcj  19801  cnfldds  19804  cnfldfun  19806  xrsadd  19811  xrsmul  19812  xrsds  19837  cnmgpid  19856  nn0srg  19864  rge0srg  19865  zring0  19876  cnmsgnsubg  19971  psgninv  19976  re0g  20006  ipffval  20041  ocvfval  20058  frlmbas  20147  mdetrlin  20456  mdetunilem9  20474  leordtval2  21064  iscnp2  21091  utop3cls  22102  nmfval  22440  nmoffn  22562  nmofval  22565  icccld  22617  addcnlem  22714  iimulcn  22784  icopnfhmeo  22789  iccpnfcnv  22790  iccpnfhmeo  22791  xrhmeo  22792  xrhmph  22793  oprpiece1res1  22797  oprpiece1res2  22798  ishtpy  22818  pcoass  22870  cnstrcvs  22987  cncvs  22991  recvs  22992  qcvs  22993  zclmncvs  22994  tchex  23062  cnfldcusp  23199  resscdrg  23200  reust  23215  recusp  23216  vitalilem4  23425  vitalilem5  23426  mbfdm  23440  dveflem  23787  dvlipcn  23802  c1lip2  23806  dgrid  24065  iaa  24125  abelthlem3  24232  abelthlem5  24234  abelth  24240  efcn  24242  sinhalfpilem  24260  sincosq1lem  24294  sincosq4sgn  24298  tangtx  24302  sincos4thpi  24310  sincos6thpi  24312  pige3  24314  relogcn  24429  dvlog2lem  24443  dvlog2  24444  logtayl  24451  logtayl2  24453  cxpsqrtlem  24493  cxpsqrt  24494  cxpcn2  24532  cxpcn3  24534  logblog  24575  ang180lem1  24584  ang180lem2  24585  1cubrlem  24613  mcubic  24619  quart1lem  24627  quart1  24628  reasinsin  24668  atancj  24682  efiatan  24684  atantan  24695  atanbndlem  24697  atan1  24700  atancn  24708  atantayl2  24710  log2cnv  24716  log2tlbnd  24717  log2ublem1  24718  log2ublem2  24719  log2ub  24721  efrlim  24741  scvxcvx  24757  1sgm2ppw  24970  ppiub  24974  bclbnd  25050  bposlem8  25061  lgsdir2lem1  25095  lgsdir2lem5  25099  lgseisenlem1  25145  lgseisenlem2  25146  lgsquadlem1  25150  chebbnd1  25206  dchrvmasumlem2  25232  istrkg3ld  25405  trgcgrg  25455  ax5seglem7  25860  axlowdimlem6  25872  axlowdimlem8  25874  axlowdimlem11  25877  cusgrsizeindb1  26402  vtxdginducedm1  26495  0grrusgr  26531  erclwwlktr  26979  erclwwlkntr  27035  wlk2v2e  27135  upgr3v3e3cycl  27158  konigsberglem1  27230  konigsberglem2  27231  konigsberglem3  27232  konigsberglem5  27234  ex-fl  27434  ex-mod  27436  ex-hash  27440  ex-lcm  27445  0vfval  27589  smcnlem  27680  lnocoi  27740  nmlno0lem  27776  nmblolbii  27782  blocnilem  27787  blocni  27788  cncph  27802  isph  27805  ip0i  27808  ip1ilem  27809  ip2i  27811  ipdirilem  27812  ipasslem7  27819  ipasslem8  27820  ipasslem9  27821  ipasslem10  27822  ipasslem11  27823  ip2dii  27827  pythi  27833  siilem1  27834  siilem2  27835  siii  27836  hvmulassi  28031  hvmulcomi  28032  hvdistr1i  28036  hvsubdistr1i  28037  hvassi  28038  hvadd32i  28039  hvsubassi  28040  hvsub32i  28041  normlem0  28094  normlem8  28102  normlem9  28103  bcseqi  28105  polid2i  28142  hhph  28163  hlim0  28220  shscli  28304  shlessi  28364  shlej1i  28365  omlsilem  28389  shlubi  28402  h1de2i  28540  pjadjii  28661  pjaddii  28662  pjmulii  28664  pjdifnormii  28670  pjcji  28671  hoaddsubassi  28807  eigrei  28821  eigposi  28823  eigorthi  28824  adj0  28981  lnopeq0lem1  28992  lnopunilem1  28997  lnophmlem2  29004  nmcexi  29013  nmcopexi  29014  lnfn0i  29029  nmcfnexi  29038  mdexchi  29322  xppreima2  29578  dp2clq  29716  dp2lt  29720  dp2ltc  29722  dpexpp1  29744  dpmul  29749  dpmul4  29750  elxrge02  29768  xrge0adddir  29820  xrnarchi  29866  xrge0slmod  29972  psgnid  29975  raddcn  30103  xrge0iifcnv  30107  xrge0iifiso  30109  xrge0iifhmeo  30110  xrge0iifhom  30111  xrge0iifmhm  30113  xrge0mulc1cn  30115  lmlimxrge0  30122  pnfneige0  30125  lmxrge0  30126  zringnm  30132  rezh  30143  qqh0  30156  qqh1  30157  qqhucn  30164  esumpinfval  30263  hashf2  30274  esumcvg  30276  br2base  30459  sxbrsigalem3  30462  dya2iocbrsiga  30465  dya2icobrsiga  30466  sxbrsigalem1  30475  sxbrsigalem2  30476  sxbrsigalem4  30477  sxbrsigalem5  30478  sxbrsiga  30480  ballotlem2  30678  ballotlem4  30688  ballotlemi1  30692  ballotth  30727  sgnclre  30729  signstf  30771  itgexpif  30812  chtvalz  30835  hgt750lemd  30854  hgt750lem  30857  tgoldbachgnn  30865  subfacp1lem1  31287  subfacp1lem6  31293  kur14lem6  31319  cvmliftlem4  31396  problem4  31688  quad3  31690  logi  31746  iexpire  31747  fununiq  31793  fvtransport  32264  bj-minftyccb  33242  taupilem2  33298  1oequni2o  33346  finxp1o  33359  finxpreclem4  33361  cos2h  33530  tan2h  33531  pigt3  33532  poimirlem9  33548  poimirlem27  33566  poimirlem28  33567  ismblfin  33580  mbfposadd  33587  ftc1anclem5  33619  asindmre  33625  dvasin  33626  dvacos  33627  rrnval  33756  el3v  34130  dihjatcclem4  37027  rabren3dioph  37696  jm2.27dlem2  37894  rmydioph  37898  rmxdioph  37900  expdiophlem2  37906  expdioph  37907  arearect  38118  areaquad  38119  corclrcl  38316  iunrelexpuztr  38328  corcltrcl  38348  dffrege76  38550  k0004val0  38769  lhe4.4ex1a  38845  binomcxplemdvbinom  38869  binomcxplemnotnn0  38872  ax6e2ndeqALT  39481  sineq0ALT  39487  pnfel0pnf  40072  lptioo2cn  40195  limsup10ex  40323  liminf10ex  40324  icccncfext  40418  itgsin0pilem1  40483  itgsbtaddcnst  40516  stoweidlem13  40548  wallispilem2  40601  wallispilem4  40603  wallispi2lem1  40606  stirlinglem13  40621  dirkerper  40631  dirkertrigeqlem3  40635  dirkeritg  40637  dirkercncflem1  40638  dirkercncflem4  40641  fourierdlem42  40684  fourierdlem62  40703  fourierdlem102  40743  fourierdlem103  40744  fourierdlem104  40745  fourierdlem114  40755  sqwvfoura  40763  fourierswlem  40765  fouriersw  40766  smfmullem4  41322  fmtnoprmfac2lem1  41803  fmtno4prm  41812  2exp5  41832  2exp11  41842  3exp4mod41  41858  41prothprmlem2  41860  6gbe  41984  7gbow  41985  8gbe  41986  9gbo  41987  11gbo  41988  sbgoldbalt  41994  nnsum4primesevenALTV  42014  0nodd  42135  oddinmgm  42140  2zrng0  42263  zlmodzxz0  42459  zlmodzxzequa  42610  zlmodzxzequap  42613  zlmodzxzldeplem3  42616  nnlog2ge0lt1  42685  blen1  42703  blen2  42704  nnolog2flm1  42709
  Copyright terms: Public domain W3C validator