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

Theorem mpani 692
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 691 1 (𝜑 → (𝜒𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  mp2ani  694  wfi  6174  ordelinel  6282  dif20el  8119  domunfican  8779  mulgt1  11487  recgt1i  11525  recreclt  11527  ledivp1i  11553  nngt0  11656  nnrecgt0  11668  elnnnn0c  11930  elnnz1  11996  recnz  12045  uz3m2nn  12279  ledivge1le  12448  xrub  12693  1mod  13259  expubnd  13529  expnbnd  13581  expnlbnd  13582  hashgt23el  13773  resqrex  14598  sin02gt0  15533  oddge22np1  15686  dvdsnprmd  16022  prmlem1  16429  prmlem2  16441  lsmss2  18722  ovolicopnf  24052  voliunlem3  24080  volsup  24084  volivth  24135  itg2seq  24270  itg2monolem2  24279  reeff1olem  24961  sinq12gt0  25020  logdivlti  25130  logdivlt  25131  efexple  25784  gausslemma2dlem4  25872  axlowdimlem16  26670  axlowdimlem17  26671  axlowdim  26674  rusgr1vtx  27297  dmdbr2  30007  dfon2lem3  32927  dfon2lem7  32931  frpoind  32977  frind  32982  nn0prpwlem  33567  bj-resta  34281  tan2h  34765  mblfinlem4  34813  m1mod0mod1  43406  iccpartgt  43464  gbegt5  43803  gbowgt5  43804  sbgoldbalt  43823  sgoldbeven3prm  43825  nnsum4primesodd  43838  nnsum4primesoddALTV  43839  evengpoap3  43841  nnsum4primesevenALTV  43843  m1modmmod  44509  difmodm1lt  44510  regt1loggt0  44524  rege1logbrege0  44546  rege1logbzge0  44547
  Copyright terms: Public domain W3C validator