ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpanl1 Unicode version

Theorem mpanl1 431
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 312 . 2  |-  ( ps 
->  ( ph  /\  ps ) )
3 mpanl1.2 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
42, 3sylan 281 1  |-  ( ( ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  mpanl12  433  ercnv  6458  rec11api  8537  divdiv23apzi  8549  recp1lt1  8681  divgt0i  8692  divge0i  8693  ltreci  8694  lereci  8695  lt2msqi  8696  le2msqi  8697  msq11i  8698  ltdiv23i  8708  fnn0ind  9191  elfzp1b  9908  elfzm1b  9909  sqrt11i  10936  sqrtmuli  10937  sqrtmsq2i  10939  sqrtlei  10940  sqrtlti  10941
  Copyright terms: Public domain W3C validator