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  328  pm5.31  348  con4biddc  858  jaddc  865  hbimd  1584  19.21ht  1592  nfimd  1596  19.23t  1688  spimth  1746  ssuni  3849  nnmordi  6545  omnimkv  7189  caucvgsrlemoffcau  7832  caucvgsrlemoffres  7834  facdiv  10759  facwordi  10761  bezoutlemmain  12040  bezoutlemaz  12045  bezoutlembz  12046  algcvgblem  12092  prmfac1  12195  infpnlem1  12402  cncfco  14563  limccnpcntop  14629  limccoap  14632  bj-rspgt  15024
  Copyright terms: Public domain W3C validator