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

Theorem mpani 679
Description: An inference based on modus ponens. (Contributed by NM, 10-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Nov-2012.)
Hypotheses
Ref Expression
mpani.1 𝜓
mpani.2 (𝜑 → ((𝜓𝜒) → 𝜃))
Assertion
Ref Expression
mpani (𝜑 → (𝜒𝜃))

Proof of Theorem mpani
StepHypRef Expression
1 mpani.1 . . 3 𝜓
21a1i 11 . 2 (𝜑𝜓)
3 mpani.2 . 2 (𝜑 → ((𝜓𝜒) → 𝜃))
42, 3mpand 678 1 (𝜑 → (𝜒𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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
This theorem is referenced by:  mp2ani  681  wfi  5933  ordelinel  6042  dif20el  7825  domunfican  8475  mulgt1  11170  recgt1i  11208  recreclt  11210  ledivp1i  11237  nngt0  11338  nnrecgt0  11347  elnnnn0c  11607  elnnz1  11672  recnz  11721  uz3m2nn  11952  ledivge1le  12118  xrub  12363  1mod  12929  expubnd  13147  expnbnd  13219  expnlbnd  13220  resqrex  14217  sin02gt0  15145  oddge22np1  15296  dvdsnprmd  15624  prmlem1  16029  prmlem2  16041  lsmss2  18285  ovolicopnf  23511  voliunlem3  23539  volsup  23543  volivth  23594  itg2seq  23729  itg2monolem2  23738  reeff1olem  24420  sinq12gt0  24480  logdivlti  24586  logdivlt  24587  efexple  25226  gausslemma2dlem4  25314  axlowdimlem16  26057  axlowdimlem17  26058  axlowdim  26061  rusgr1vtx  26718  dmdbr2  29496  dfon2lem3  32015  dfon2lem7  32019  frpoind  32066  frind  32069  nn0prpwlem  32643  bj-resta  33362  tan2h  33716  mblfinlem4  33764  m1mod0mod1  41915  iccpartgt  41939  pfx2  41988  gbegt5  42225  gbowgt5  42226  sbgoldbalt  42245  sgoldbeven3prm  42247  nnsum4primesodd  42260  nnsum4primesoddALTV  42261  evengpoap3  42263  nnsum4primesevenALTV  42265  m1modmmod  42885  difmodm1lt  42886  regt1loggt0  42899  rege1logbrege0  42921  rege1logbzge0  42922
  Copyright terms: Public domain W3C validator