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

Theorem mp3an13 1328
Description: An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.)
Hypotheses
Ref Expression
mp3an13.1  |-  ph
mp3an13.2  |-  ch
mp3an13.3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Assertion
Ref Expression
mp3an13  |-  ( ps 
->  th )

Proof of Theorem mp3an13
StepHypRef Expression
1 mp3an13.1 . 2  |-  ph
2 mp3an13.2 . . 3  |-  ch
3 mp3an13.3 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
42, 3mp3an3 1326 . 2  |-  ( (
ph  /\  ps )  ->  th )
51, 4mpan 424 1  |-  ( ps 
->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 978
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117  df-3an 980
This theorem is referenced by:  pitonnlem1p1  7833  mulid1  7942  addltmul  9141  eluzaddi  9540  fz01en  10036  fznatpl1  10059  expubnd  10560  bernneq  10623  bernneq2  10624  efi4p  11706  efival  11721  cos2tsin  11740  cos01bnd  11747  cos01gt0  11751  dvds0  11794  odd2np1  11858  opoe  11880  gcdid  11967  pythagtriplem4  12248  blssioo  13705  tgioo  13706  rerestcntop  13710  sinperlem  13889  sincosq1sgn  13907  sincosq2sgn  13908  sinq12gt0  13911  cosq14gt0  13913
  Copyright terms: Public domain W3C validator