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

Theorem imim2d 54
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-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  imim2  55  embantd  56  imim12d  74  anc2r  326  pm5.31  346  con4biddc  843  jaddc  850  hbimd  1553  19.21ht  1561  nfimd  1565  19.23t  1657  spimth  1715  ssuni  3796  nnmordi  6465  omnimkv  7101  caucvgsrlemoffcau  7720  caucvgsrlemoffres  7722  facdiv  10623  facwordi  10625  bezoutlemmain  11897  bezoutlemaz  11902  bezoutlembz  11903  algcvgblem  11941  prmfac1  12042  cncfco  13048  limccnpcntop  13114  limccoap  13117  bj-rspgt  13431
  Copyright terms: Public domain W3C validator