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  6175  ordelinel  6283  dif20el  8121  domunfican  8780  mulgt1  11488  recgt1i  11526  recreclt  11528  ledivp1i  11554  nngt0  11657  nnrecgt0  11669  elnnnn0c  11931  elnnz1  11997  recnz  12046  uz3m2nn  12280  ledivge1le  12450  xrub  12695  1mod  13261  expubnd  13531  expnbnd  13583  expnlbnd  13584  hashgt23el  13775  resqrex  14600  sin02gt0  15535  oddge22np1  15688  dvdsnprmd  16024  prmlem1  16431  prmlem2  16443  lsmss2  18724  ovolicopnf  24054  voliunlem3  24082  volsup  24086  volivth  24137  itg2seq  24272  itg2monolem2  24281  reeff1olem  24963  sinq12gt0  25022  logdivlti  25130  logdivlt  25131  efexple  25785  gausslemma2dlem4  25873  axlowdimlem16  26671  axlowdimlem17  26672  axlowdim  26675  rusgr1vtx  27298  dmdbr2  30008  dfon2lem3  32928  dfon2lem7  32932  frpoind  32978  frind  32983  nn0prpwlem  33568  bj-resta  34282  tan2h  34766  mblfinlem4  34814  m1mod0mod1  43410  iccpartgt  43434  gbegt5  43773  gbowgt5  43774  sbgoldbalt  43793  sgoldbeven3prm  43795  nnsum4primesodd  43808  nnsum4primesoddALTV  43809  evengpoap3  43811  nnsum4primesevenALTV  43813  m1modmmod  44479  difmodm1lt  44480  regt1loggt0  44494  rege1logbrege0  44516  rege1logbzge0  44517
  Copyright terms: Public domain W3C validator