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

Theorem mpanl1 684
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 543 . 2  |-  ( ps 
->  ( ph  /\  ps ) )
3 mpanl1.2 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
42, 3sylan 473 1  |-  ( ( ps  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  mpanl12  686  frc  4820  oeoelem  7307  ercnv  7392  frfi  7822  fin23lem23  8754  divdiv23zi  10359  recp1lt1  10504  divgt0i  10515  divge0i  10516  ltreci  10517  lereci  10518  lt2msqi  10519  le2msqi  10520  msq11i  10521  ltdiv23i  10531  fnn0ind  11034  elfzp1b  11869  elfzm1b  11870  sqrt11i  13426  sqrtmuli  13427  sqrtmsq2i  13429  sqrtlei  13430  sqrtlti  13431  fsum  13764  fprod  13973  blometi  26289  spansnm0i  27138  lnopli  27456  lnfnli  27528  opsqrlem1  27628  opsqrlem6  27633  mdslmd3i  27820  atordi  27872  mdsymlem1  27891  gsummpt2co  28381  ptrecube  31644  fdc  31778  prter3  32162
  Copyright terms: Public domain W3C validator