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

Theorem mpani 714
 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 713 1 (𝜑 → (𝜒𝜃))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383 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 This theorem is referenced by:  mp2ani  716  wfi  5874  ordelinel  5986  ordelinelOLD  5987  dif20el  7756  domunfican  8400  mulgt1  11094  recgt1i  11132  recreclt  11134  ledivp1i  11161  nngt0  11261  nnrecgt0  11270  elnnnn0c  11550  elnnz1  11615  recnz  11664  uz3m2nn  11944  ledivge1le  12114  xrub  12355  1mod  12916  expubnd  13135  expnbnd  13207  expnlbnd  13208  resqrex  14210  sin02gt0  15141  oddge22np1  15295  dvdsnprmd  15625  prmlem1  16036  prmlem2  16049  lsmss2  18301  ovolicopnf  23512  voliunlem3  23540  volsup  23544  volivth  23595  itg2seq  23728  itg2monolem2  23737  reeff1olem  24419  sinq12gt0  24479  logdivlti  24586  logdivlt  24587  efexple  25226  gausslemma2dlem4  25314  axlowdimlem16  26057  axlowdimlem17  26058  axlowdim  26061  rusgr1vtx  26715  dmdbr2  29492  dfon2lem3  32016  dfon2lem7  32020  frpoind  32067  frind  32070  nn0prpwlem  32644  bj-resta  33373  tan2h  33732  mblfinlem4  33780  m1mod0mod1  41867  iccpartgt  41891  pfx2  41940  gbegt5  42177  gbowgt5  42178  sbgoldbalt  42197  sgoldbeven3prm  42199  nnsum4primesodd  42212  nnsum4primesoddALTV  42213  evengpoap3  42215  nnsum4primesevenALTV  42217  m1modmmod  42844  difmodm1lt  42845  regt1loggt0  42858  rege1logbrege0  42880  rege1logbzge0  42881
 Copyright terms: Public domain W3C validator