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

Theorem mp3an23 1307
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 1304 . 2  |-  ( (
ph  /\  ps )  ->  th )
51, 4mpan2 421 1  |-  ( ph  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 962
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 964
This theorem is referenced by:  sbciegf  2940  ac6sfi  6792  dju0en  7070  1qec  7203  ltaddnq  7222  halfnqq  7225  1idsr  7583  pn0sr  7586  ltm1sr  7592  muleqadd  8436  halfcl  8953  rehalfcl  8954  half0  8955  2halves  8956  halfpos2  8957  halfnneg2  8959  halfaddsub  8961  nneoor  9160  zeo  9163  fztp  9865  modqfrac  10117  iexpcyc  10404  bcn2  10517  bcpasc  10519  imre  10630  reim  10631  crim  10637  addcj  10670  imval2  10673  sinf  11418  efi4p  11431  resin4p  11432  recos4p  11433  sinneg  11440  efival  11446  cosadd  11451  sinmul  11458  sinbnd  11466  cosbnd  11467  ef01bndlem  11470  sin01bnd  11471  cos01bnd  11472  sin01gt0  11475  cos01gt0  11476  sin02gt0  11477  odd2np1lem  11576  odd2np1  11577  mopnex  12684  sincosq1lem  12919  sincosq2sgn  12921  sincosq3sgn  12922  sincosq4sgn  12923  sinq12gt0  12924  abssinper  12940  coskpi  12942
  Copyright terms: Public domain W3C validator