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

Theorem imim2d 48
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 23 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  49  embantd  50  imim12d  68  anc2r  311  pm5.31  330  con4biddc  754  jaddc  761  hbimd  1465  19.21ht  1473  nfimd  1477  19.23t  1567  spimth  1623  ssuni  3602  nnmordi  6089  caucvgsrlemoffcau  6882  caucvgsrlemoffres  6884  algcvgblem  9888  bj-rspgt  9925
  Copyright terms: Public domain W3C validator