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

Theorem a2i 11
Description: Inference derived from axiom ax-2 6. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
a2i.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
a2i  |-  ( (
ph  ->  ps )  -> 
( ph  ->  ch )
)

Proof of Theorem a2i
StepHypRef Expression
1 a2i.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 ax-2 6 . 2  |-  ( (
ph  ->  ( ps  ->  ch ) )  ->  (
( ph  ->  ps )  ->  ( ph  ->  ch ) ) )
31, 2ax-mp 7 1  |-  ( (
ph  ->  ps )  -> 
( ph  ->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-2 6  ax-mp 7
This theorem is referenced by:  imim2i  12  mpd  13  sylcom  28  pm2.43  52  ancl  311  ancr  314  anc2r  321  pm2.65  620  pm2.18dc  788  con4biddc  792  hbim1  1507  sbcof2  1738  ralimia  2436  ceqsalg  2647  rspct  2715  elabgt  2755  fvmptt  5378  ordiso2  6707  bj-exlimmp  11327  bj-rspgt  11343  bj-indint  11483
  Copyright terms: Public domain W3C validator