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

Theorem imp31 243
 Description: An importation inference. (Contributed by NM, 26-Apr-1994.)
Hypothesis
Ref Expression
imp3.1 (𝜑 → (𝜓 → (𝜒𝜃)))
Assertion
Ref Expression
imp31 (((𝜑𝜓) ∧ 𝜒) → 𝜃)

Proof of Theorem imp31
StepHypRef Expression
1 imp3.1 . . 3 (𝜑 → (𝜓 → (𝜒𝜃)))
21imp 115 . 2 ((𝜑𝜓) → (𝜒𝜃))
32imp 115 1 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100 This theorem is referenced by:  imp41  335  imp5d  341  impl  362  anassrs  380  an31s  504  con4biddc  754  3imp  1098  3expa  1104  bilukdc  1287  reusv3  4192  dfimafn  5222  funimass4  5224  funimass3  5283  isopolem  5461  smores2  5909  tfrlem9  5935  nnmordi  6089  mulcanpig  6433  elnnz  8255  irradd  8580  irrmul  8581  uzsubsubfz  8911  fzo1fzo0n0  9039  elfzonelfzo  9086
 Copyright terms: Public domain W3C validator