ILE Home 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  6431  elnnz  8253  irradd  8578  irrmul  8579  uzsubsubfz  8909  fzo1fzo0n0  9037  elfzonelfzo  9084
  Copyright terms: Public domain W3C validator