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

Theorem mpanl1 661
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  |-  ph
mpanl1.2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Assertion
Ref Expression
mpanl1  |-  ( ( ps  /\  ch )  ->  th )

Proof of Theorem mpanl1
StepHypRef Expression
1 mpanl1.1 . . 3  |-  ph
21jctl 525 . 2  |-  ( ps 
->  ( ph  /\  ps ) )
3 mpanl1.2 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
42, 3sylan 457 1  |-  ( ( ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  mpanl12  663  frc  4359  oeoelem  6596  ercnv  6681  frfi  7102  fin23lem23  7952  divdiv23zi  9513  recp1lt1  9654  divgt0i  9665  divge0i  9666  ltreci  9667  lereci  9668  lt2msqi  9669  le2msqi  9670  msq11i  9671  ltdiv23i  9681  fnn0ind  10111  elfzm1b  10860  sqr11i  11868  sqrmuli  11869  sqrmsq2i  11871  sqrlei  11872  sqrlti  11873  fsum  12193  blometi  21381  spansnm0i  22229  lnopli  22548  lnfnli  22620  opsqrlem1  22720  opsqrlem6  22725  mdslmd3i  22912  atordi  22964  mdsymlem1  22983  elfzp1b  24012  fdc  26455  prter3  26750
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator