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  345  con4biddc  827  jaddc  834  hbimd  1537  19.21ht  1545  nfimd  1549  19.23t  1640  spimth  1698  ssuni  3728  nnmordi  6380  omnimkv  6998  caucvgsrlemoffcau  7574  caucvgsrlemoffres  7576  facdiv  10452  facwordi  10454  bezoutlemmain  11613  bezoutlemaz  11618  bezoutlembz  11619  algcvgblem  11657  prmfac1  11757  cncfco  12674  limccnpcntop  12740  limccoap  12743  bj-rspgt  12920
  Copyright terms: Public domain W3C validator