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

Theorem imp31 247
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 119 . 2 ((𝜑𝜓) → (𝜒𝜃))
32imp 119 1 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104
This theorem is referenced by:  imp41  339  imp5d  345  impl  366  anassrs  386  an31s  512  con4biddc  763  3imp  1107  3expa  1113  bilukdc  1301  reusv3  4217  dfimafn  5247  funimass4  5249  funimass3  5308  isopolem  5486  smores2  5937  tfrlem9  5963  nnmordi  6117  mulcanpig  6461  elnnz  8282  nzadd  8324  irradd  8648  irrmul  8649  uzsubsubfz  8983  fzo1fzo0n0  9111  elfzonelfzo  9158
  Copyright terms: Public domain W3C validator