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

Theorem imim2d 53
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  54  embantd  55  imim12d  73  anc2r  321  pm5.31  340  con4biddc  792  jaddc  799  hbimd  1510  19.21ht  1518  nfimd  1522  19.23t  1612  spimth  1670  ssuni  3670  nnmordi  6255  caucvgsrlemoffcau  7322  caucvgsrlemoffres  7324  facdiv  10111  facwordi  10113  bezoutlemmain  11080  bezoutlemaz  11085  bezoutlembz  11086  algcvgblem  11124  prmfac1  11224  bj-rspgt  11343
  Copyright terms: Public domain W3C validator