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

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
StepHypRef Expression
1 mpanl1.1 . . 3
21jctl 541 . 2
3 mpanl1.2 . 2
42, 3sylan 471 1
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator