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

Theorem mpani 711
 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 710 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 197  df-an 386 This theorem is referenced by:  mp2ani  713  wfi  5701  ordelinel  5813  ordelinelOLD  5814  dif20el  7570  domunfican  8218  mulgt1  10867  recgt1i  10905  recreclt  10907  ledivp1i  10934  nngt0  11034  nnrecgt0  11043  elnnnn0c  11323  elnnz1  11388  recnz  11437  uz3m2nn  11716  ledivge1le  11886  xrub  12127  1mod  12685  expubnd  12904  expnbnd  12976  expnlbnd  12977  resqrex  13972  sin02gt0  14903  oddge22np1  15054  dvdsnprmd  15384  prmlem1  15795  prmlem2  15808  lsmss2  18062  ovolicopnf  23273  voliunlem3  23301  volsup  23305  volivth  23356  itg2seq  23490  itg2monolem2  23499  reeff1olem  24181  sinq12gt0  24240  logdivlti  24347  logdivlt  24348  efexple  24987  gausslemma2dlem4  25075  axlowdimlem16  25818  axlowdimlem17  25819  axlowdim  25822  rusgr1vtx  26465  dmdbr2  29132  dfon2lem3  31664  dfon2lem7  31668  frind  31714  nn0prpwlem  32292  bj-resta  33024  tan2h  33372  mblfinlem4  33420  m1mod0mod1  41103  iccpartgt  41127  pfx2  41177  gbegt5  41414  gbowgt5  41415  sbgoldbalt  41434  sgoldbeven3prm  41436  nnsum4primesodd  41449  nnsum4primesoddALTV  41450  evengpoap3  41452  nnsum4primesevenALTV  41454  m1modmmod  42081  difmodm1lt  42082  regt1loggt0  42095  rege1logbrege0  42117  rege1logbzge0  42118
 Copyright terms: Public domain W3C validator