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

Theorem mp3an13 1318
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 1316 . 2  |-  ( (
ph  /\  ps )  ->  th )
51, 4mpan 421 1  |-  ( ps 
->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 968
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 depends on definitions:  df-bi 116  df-3an 970
This theorem is referenced by:  pitonnlem1p1  7787  mulid1  7896  addltmul  9093  eluzaddi  9492  fz01en  9988  fznatpl1  10011  expubnd  10512  bernneq  10575  bernneq2  10576  efi4p  11658  efival  11673  cos2tsin  11692  cos01bnd  11699  cos01gt0  11703  dvds0  11746  odd2np1  11810  opoe  11832  gcdid  11919  pythagtriplem4  12200  blssioo  13195  tgioo  13196  rerestcntop  13200  sinperlem  13379  sincosq1sgn  13397  sincosq2sgn  13398  sinq12gt0  13401  cosq14gt0  13403
  Copyright terms: Public domain W3C validator