Theorem mpanl1 680

Description: An inference based on modus ponens. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)

Hypotheses

Ref	Expression
mpanl1.1
mpanl1.2

Assertion

Ref	Expression
mpanl1

Proof of Theorem mpanl1

Step	Hyp	Ref	Expression
1		mpanl1.1	. . 3
2	1	jctl 541	. 2
3		mpanl1.2	. 2
4	2, 3	sylan 471	1

Syntax hints:  ->wi 4  /\wa 369

This theorem is referenced by:  mpanl12  682  frc  4850  oeoelem  7266  ercnv  7351  frfi  7785  fin23lem23  8727  divdiv23zi  10322  recp1lt1  10468  divgt0i  10479  divge0i  10480  ltreci  10481  lereci  10482  lt2msqi  10483  le2msqi  10484  msq11i  10485  ltdiv23i  10495  fnn0ind  10988  elfzp1b  11784  elfzm1b  11785  sqrt11i  13217  sqrtmuli  13218  sqrtmsq2i  13220  sqrtlei  13221  sqrtlti  13222  fsum  13542  fprod  13748  blometi  25718  spansnm0i  26568  lnopli  26887  lnfnli  26959  opsqrlem1  27059  opsqrlem6  27064  mdslmd3i  27251  atordi  27303  mdsymlem1  27322  gsummpt2co  27771  fdc  30238  prter3  30623

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