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 7. (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 7 . 2  |-  ( (
ph  ->  ( ps  ->  ch ) )  ->  (
( ph  ->  ps )  ->  ( ph  ->  ch ) ) )
31, 2ax-mp 5 1  |-  ( (
ph  ->  ps )  -> 
( ph  ->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-2 7
This theorem is referenced by:  imim2i  12  mpd  13  sylcom  28  pm2.43  53  ancl  318  ancr  321  anc2r  328  pm2.65  660  pm2.18dc  856  con4biddc  858  hbim1  1581  sbcof2  1821  ralimia  2551  ceqsalg  2780  rspct  2849  elabgt  2893  fvmptt  5631  ordiso2  7068  bj-exlimmp  15007  bj-rspgt  15024  bj-indint  15169
  Copyright terms: Public domain W3C validator