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

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

Proof of Theorem mp3an23
StepHypRef Expression
1 mp3an23.1 . 2  |-  ps
2 mp3an23.2 . . 3  |-  ch
3 mp3an23.3 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
42, 3mp3an3 1262 . 2  |-  ( (
ph  /\  ps )  ->  th )
51, 4mpan2 416 1  |-  ( ph  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 924
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115  df-3an 926
This theorem is referenced by:  sbciegf  2868  ac6sfi  6594  1qec  6926  ltaddnq  6945  halfnqq  6948  1idsr  7293  pn0sr  7296  muleqadd  8111  halfcl  8612  rehalfcl  8613  half0  8614  2halves  8615  halfpos2  8616  halfnneg2  8618  halfaddsub  8620  nneoor  8818  zeo  8821  fztp  9459  modqfrac  9709  iexpcyc  10024  bcn2  10137  bcpasc  10139  imre  10250  reim  10251  crim  10257  addcj  10290  imval2  10293  odd2np1lem  10965  odd2np1  10966
  Copyright terms: Public domain W3C validator