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

Theorem mpani 695
 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 694 1 (𝜑 → (𝜒𝜃))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399 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 210  df-an 400 This theorem is referenced by:  mp2ani  697  wfi  6168  ordelinel  6276  dif20el  8126  domunfican  8788  mulgt1  11497  recgt1i  11535  recreclt  11537  ledivp1i  11563  nngt0  11665  nnrecgt0  11677  elnnnn0c  11939  elnnz1  12005  recnz  12054  uz3m2nn  12288  ledivge1le  12457  xrub  12702  1mod  13275  expubnd  13546  expnbnd  13598  expnlbnd  13599  hashgt23el  13790  resqrex  14610  sin02gt0  15545  oddge22np1  15698  dvdsnprmd  16032  prmlem1  16441  prmlem2  16453  lsmss2  18793  ovolicopnf  24134  voliunlem3  24162  volsup  24166  volivth  24217  itg2seq  24352  itg2monolem2  24361  reeff1olem  25047  sinq12gt0  25106  logdivlti  25217  logdivlt  25218  efexple  25871  gausslemma2dlem4  25959  axlowdimlem16  26757  axlowdimlem17  26758  axlowdim  26761  rusgr1vtx  27384  dmdbr2  30092  dfon2lem3  33090  dfon2lem7  33094  frpoind  33140  frind  33145  nn0prpwlem  33730  bj-resta  34458  tan2h  34997  mblfinlem4  35045  m1mod0mod1  43816  iccpartgt  43874  gbegt5  44209  gbowgt5  44210  sbgoldbalt  44229  sgoldbeven3prm  44231  nnsum4primesodd  44244  nnsum4primesoddALTV  44245  evengpoap3  44247  nnsum4primesevenALTV  44249  m1modmmod  44865  difmodm1lt  44866  regt1loggt0  44880  rege1logbrege0  44902  rege1logbzge0  44903
 Copyright terms: Public domain W3C validator