MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpanl1 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  4482  oeoelem  6770  ercnv  6855  frfi  7281  fin23lem23  8132  divdiv23zi  9692  recp1lt1  9833  divgt0i  9844  divge0i  9845  ltreci  9846  lereci  9847  lt2msqi  9848  le2msqi  9849  msq11i  9850  ltdiv23i  9860  fnn0ind  10294  elfzm1b  11048  sqr11i  12108  sqrmuli  12109  sqrmsq2i  12111  sqrlei  12112  sqrlti  12113  fsum  12434  blometi  22145  spansnm0i  22993  lnopli  23312  lnfnli  23384  opsqrlem1  23484  opsqrlem6  23489  mdslmd3i  23676  atordi  23728  mdsymlem1  23747  elfzp1b  24888  fprod  25039  fdc  26133  prter3  26415
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