MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpanl1 Structured version   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  |-  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 541 . 2  |-  ( ps 
->  ( ph  /\  ps ) )
3 mpanl1.2 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
42, 3sylan 471 1  |-  ( ( ps  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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
This theorem is referenced by:  mpanl12  682  frc  4845  oeoelem  7247  ercnv  7332  frfi  7765  fin23lem23  8706  divdiv23zi  10297  recp1lt1  10443  divgt0i  10454  divge0i  10455  ltreci  10456  lereci  10457  lt2msqi  10458  le2msqi  10459  msq11i  10460  ltdiv23i  10470  fnn0ind  10960  elfzp1b  11755  elfzm1b  11756  sqrt11i  13180  sqrtmuli  13181  sqrtmsq2i  13183  sqrtlei  13184  sqrtlti  13185  fsum  13505  blometi  25422  spansnm0i  26272  lnopli  26591  lnfnli  26663  opsqrlem1  26763  opsqrlem6  26768  mdslmd3i  26955  atordi  27007  mdsymlem1  27026  gsummpt2co  27462  fprod  28678  fdc  29869  prter3  30255
  Copyright terms: Public domain W3C validator