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  53  ancl  312  ancr  315  anc2r  322  pm2.65  621  pm2.18dc  789  con4biddc  793  hbim1  1508  sbcof2  1739  ralimia  2437  ceqsalg  2648  rspct  2716  elabgt  2758  fvmptt  5407  ordiso2  6782  bj-exlimmp  11936  bj-rspgt  11952  bj-indint  12092
  Copyright terms: Public domain W3C validator