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

Theorem mpani 707
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 706 1 (𝜑 → (𝜒𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  mp2ani  709  wfi  5613  ordelinel  5725  ordelinelOLD  5726  dif20el  7446  domunfican  8092  mulgt1  10728  recgt1i  10766  recreclt  10768  ledivp1i  10795  nngt0  10893  nnrecgt0  10902  elnnnn0c  11182  elnnz1  11233  recnz  11281  uz3m2nn  11560  ledivge1le  11730  xrub  11967  1mod  12516  expubnd  12735  expnbnd  12807  expnlbnd  12808  resqrex  13782  sin02gt0  14704  oddge22np1  14854  dvdsnprmd  15184  prmlem1  15595  prmlem2  15608  lsmss2  17847  ovolicopnf  23013  voliunlem3  23041  volsup  23045  volivth  23095  itg2seq  23229  itg2monolem2  23238  reeff1olem  23918  sinq12gt0  23977  logdivlti  24084  logdivlt  24085  efexple  24720  gausslemma2dlem4  24808  axlowdimlem16  25552  axlowdimlem17  25553  axlowdim  25556  dmdbr2  28349  dfon2lem3  30737  dfon2lem7  30741  frind  30787  nn0prpwlem  31290  bj-resta  32030  tan2h  32371  mblfinlem4  32419  m1mod0mod1  39751  iccpartgt  39767  gbegt5  39985  gbogt5  39986  sgoldbalt  40005  nnsum4primesodd  40014  nnsum4primesoddALTV  40015  evengpoap3  40017  nnsum4primesevenALTV  40019  pfx2  40077  rusgr1vtx  40787  frgrwopreglem2  41481  m1modmmod  42109  difmodm1lt  42110  regt1loggt0  42127  rege1logbrege0  42149  rege1logbzge0  42150
  Copyright terms: Public domain W3C validator