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

Theorem imp32 244
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 242 . 2 (φ → ((ψ χ) → θ))
32imp 115 1 ((φ (ψ χ)) → θ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100
This theorem is referenced by:  imp42  336  impr  361  anasss  379  an13s  501  3expb  1104  reuss2  3211  reupick  3215  po2nr  4037  fvmptt  5205  fliftfund  5380  f1ocnv2d  5646  addclpi  6311  addnidpig  6320  mulnqprl  6549  mulnqpru  6550  ltsubrp  8392  ltaddrp  8393
  Copyright terms: Public domain W3C validator