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

Step	Hyp	Ref	Expression
1		mpanr2.1	. . 3
2	1	jctr 542	. 2
3		mpanr2.2	. 2
4	2, 3	sylan2 474	1

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