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  4375  oeoelem  6612  ercnv  6697  frfi  7118  fin23lem23  7968  divdiv23zi  9529  recp1lt1  9670  divgt0i  9681  divge0i  9682  ltreci  9683  lereci  9684  lt2msqi  9685  le2msqi  9686  msq11i  9687  ltdiv23i  9697  fnn0ind  10127  elfzm1b  10876  sqr11i  11884  sqrmuli  11885  sqrmsq2i  11887  sqrlei  11888  sqrlti  11889  fsum  12209  blometi  21397  spansnm0i  22245  lnopli  22564  lnfnli  22636  opsqrlem1  22736  opsqrlem6  22741  mdslmd3i  22928  atordi  22980  mdsymlem1  22999  elfzp1b  24027  fprod  24164  fdc  26558  prter3  26853
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