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

Theorem mpanl1 662
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 526 . 2  |-  ( ps 
->  ( ph  /\  ps ) )
3 mpanl1.2 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
42, 3sylan 458 1  |-  ( ( ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  mpanl12  664  frc  4540  oeoelem  6833  ercnv  6918  frfi  7344  fin23lem23  8198  divdiv23zi  9759  recp1lt1  9900  divgt0i  9911  divge0i  9912  ltreci  9913  lereci  9914  lt2msqi  9915  le2msqi  9916  msq11i  9917  ltdiv23i  9927  fnn0ind  10361  elfzm1b  11117  sqr11i  12180  sqrmuli  12181  sqrmsq2i  12183  sqrlei  12184  sqrlti  12185  fsum  12506  blometi  22296  spansnm0i  23144  lnopli  23463  lnfnli  23535  opsqrlem1  23635  opsqrlem6  23640  mdslmd3i  23827  atordi  23879  mdsymlem1  23898  elfzp1b  25108  fprod  25259  fdc  26440  prter3  26722
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 178  df-an 361
  Copyright terms: Public domain W3C validator