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

Theorem imp31 252
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 122 . 2 ((𝜑𝜓) → (𝜒𝜃))
32imp 122 1 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105
This theorem is referenced by:  imp41  345  imp5d  351  impl  372  anassrs  392  an31s  537  con4biddc  792  3imp  1137  3expa  1143  bilukdc  1332  reusv3  4282  dfimafn  5353  funimass4  5355  funimass3  5415  isopolem  5601  smores2  6059  tfrlem9  6084  nnmordi  6273  mulcanpig  6892  elnnz  8758  nzadd  8800  irradd  9129  irrmul  9130  uzsubsubfz  9459  fzo1fzo0n0  9590  elfzonelfzo  9637
  Copyright terms: Public domain W3C validator