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

Theorem imp31 254
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 123 . 2 ((𝜑𝜓) → (𝜒𝜃))
32imp 123 1 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106
This theorem is referenced by:  imp41  350  imp5d  356  impl  377  anassrs  397  an31s  559  con4biddc  842  3imp  1175  3expa  1181  bilukdc  1374  reusv3  4376  dfimafn  5463  funimass4  5465  funimass3  5529  isopolem  5716  smores2  6184  tfrlem9  6209  nnmordi  6405  mulcanpig  7136  elnnz  9057  nzadd  9099  irradd  9431  irrmul  9432  uzsubsubfz  9820  fzo1fzo0n0  9953  elfzonelfzo  10000  tgcl  12218
  Copyright terms: Public domain W3C validator