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

Theorem imim2d 52
Description: Deduction adding nested antecedents. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
imim2d.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
imim2d  |-  ( ph  ->  ( ( th  ->  ps )  ->  ( th  ->  ch ) ) )

Proof of Theorem imim2d
StepHypRef Expression
1 imim2d.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
21a1d 22 . 2  |-  ( ph  ->  ( th  ->  ( ps  ->  ch ) ) )
32a2d 26 1  |-  ( ph  ->  ( ( th  ->  ps )  ->  ( th  ->  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7
This theorem is referenced by:  imim2  53  embantd  54  imim12d  72  anc2r  315  pm5.31  334  con4biddc  765  jaddc  772  hbimd  1481  19.21ht  1489  nfimd  1493  19.23t  1583  spimth  1639  ssuni  3630  nnmordi  6120  caucvgsrlemoffcau  6940  caucvgsrlemoffres  6942  facdiv  9606  facwordi  9608  algcvgblem  10271  bj-rspgt  10312
  Copyright terms: Public domain W3C validator