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  25  pm2.43  47  ancl  301  ancr  304  anc2r  311  pm2.65  585  pm2.18dc  750  con4biddc  754  hbim1  1462  sbcof2  1691  ralimia  2382  ceqsalg  2582  rspct  2649  elabgt  2684  fvmptt  5262  ordiso2  6357  bj-exlimmp  9909  bj-rspgt  9925  bj-indint  10055
  Copyright terms: Public domain W3C validator