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

Theorem imim2d 54
Description: Deduction adding nested antecedents. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
imim2d.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
imim2d (𝜑 → ((𝜃𝜓) → (𝜃𝜒)))

Proof of Theorem imim2d
StepHypRef Expression
1 imim2d.1 . . 3 (𝜑 → (𝜓𝜒))
21a1d 22 . 2 (𝜑 → (𝜃 → (𝜓𝜒)))
32a2d 26 1 (𝜑 → ((𝜃𝜓) → (𝜃𝜒)))
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  852  jaddc  859  hbimd  1566  19.21ht  1574  nfimd  1578  19.23t  1670  spimth  1728  ssuni  3816  nnmordi  6492  omnimkv  7128  caucvgsrlemoffcau  7747  caucvgsrlemoffres  7749  facdiv  10659  facwordi  10661  bezoutlemmain  11940  bezoutlemaz  11945  bezoutlembz  11946  algcvgblem  11990  prmfac1  12093  infpnlem1  12298  cncfco  13331  limccnpcntop  13397  limccoap  13400  bj-rspgt  13780
  Copyright terms: Public domain W3C validator