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

Theorem imim2d 53
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-1 5  ax-2 6  ax-mp 7
This theorem is referenced by:  imim2  54  embantd  55  imim12d  73  anc2r  321  pm5.31  340  con4biddc  788  jaddc  795  hbimd  1506  19.21ht  1514  nfimd  1518  19.23t  1608  spimth  1665  ssuni  3649  nnmordi  6205  caucvgsrlemoffcau  7246  caucvgsrlemoffres  7248  facdiv  9981  facwordi  9983  bezoutlemmain  10767  bezoutlemaz  10772  bezoutlembz  10773  algcvgblem  10811  prmfac1  10911  bj-rspgt  11029
  Copyright terms: Public domain W3C validator