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  843  jaddc  850  hbimd  1553  19.21ht  1561  nfimd  1565  19.23t  1656  spimth  1714  ssuni  3765  nnmordi  6419  omnimkv  7037  caucvgsrlemoffcau  7629  caucvgsrlemoffres  7631  facdiv  10515  facwordi  10517  bezoutlemmain  11720  bezoutlemaz  11725  bezoutlembz  11726  algcvgblem  11764  prmfac1  11864  cncfco  12784  limccnpcntop  12850  limccoap  12853  bj-rspgt  13162
  Copyright terms: Public domain W3C validator