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

Theorem imp32 253
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 251 . 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:  imp42  346  impr  371  anasss  391  an13s  534  3expb  1144  reuss2  3279  reupick  3283  po2nr  4136  fvmptt  5394  fliftfund  5576  f1ocnv2d  5848  addclpi  6884  addnidpig  6893  mulnqprl  7125  mulnqpru  7126  ltsubrp  9166  ltaddrp  9167  divgcdcoprm0  11357
  Copyright terms: Public domain W3C validator