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

Theorem mpani 676
 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 675 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  /\wa 369 This theorem is referenced by:  mp2ani  678  ordelinel  4981  dif20el  7174  domunfican  7813  mulgt1  10426  recgt1i  10467  recreclt  10469  ledivp1i  10496  nngt0  10590  nnrecgt0  10598  elnnnn0c  10866  elnnz1  10915  recnz  10963  uz3m2nn  11152  xrub  11532  1mod  12028  expubnd  12226  expnbnd  12295  expnlbnd  12296  resqrex  13084  sin02gt0  13927  prmlem1  14593  prmlem2  14605  lsmss2  16686  ovolicopnf  21935  voliunlem3  21962  volsup  21966  volivth  22016  itg2seq  22149  itg2monolem2  22158  reeff1olem  22841  sinq12gt0  22900  logdivlti  23005  logdivlt  23006  efexple  23556  axlowdimlem16  24260  axlowdimlem17  24261  axlowdim  24264  dmdbr2  27222  dfon2lem3  29217  dfon2lem7  29221  wfi  29287  frind  29323  tan2h  30047  mblfinlem4  30054  nn0prpwlem  30140 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 185  df-an 371
 Copyright terms: Public domain W3C validator