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

Theorem mpanr2 684
 Description: An inference based on modus ponens. (Contributed by NM, 3-May-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)
Hypotheses
Ref Expression
mpanr2.1
mpanr2.2
Assertion
Ref Expression
mpanr2

Proof of Theorem mpanr2
StepHypRef Expression
1 mpanr2.1 . . 3
21jctr 542 . 2
3 mpanr2.2 . 2
42, 3sylan2 474 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  /\wa 369 This theorem is referenced by:  fvreseq1  5988  op1steq  6842  fpmg  7464  pmresg  7466  pw2f1o  7642  pm54.43  8402  dfac2  8532  ttukeylem6  8915  gruina  9217  muleqadd  10218  divdiv1  10280  addltmul  10799  elfzp1b  11784  elfzm1b  11785  expp1z  12214  expm1  12215  oddvdsnn0  16568  efgi0  16738  efgi1  16739  fiinbas  19453  opnneissb  19615  fclscf  20526  blssec  20938  iimulcl  21437  itg2lr  22137  blocnilem  25719  lnopmul  26886  opsqrlem6  27064  gsumle  27770  gsumvsca1  27773  gsumvsca2  27774  locfinreflem  27843  fvray  29791  fvline  29794  fneref  30168  fdc  30238  rmyeq0  30891  linepmap  35499 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