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

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

Proof of Theorem imp32
StepHypRef Expression
1 imp3.1 . . 3 (𝜑 → (𝜓 → (𝜒𝜃)))
21impd 246 . 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:  imp42  340  impr  365  anasss  385  an13s  509  3expb  1116  reuss2  3245  reupick  3249  po2nr  4074  fvmptt  5290  fliftfund  5465  f1ocnv2d  5732  addclpi  6483  addnidpig  6492  mulnqprl  6724  mulnqpru  6725  ltsubrp  8715  ltaddrp  8716
  Copyright terms: Public domain W3C validator