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

Theorem exp32 351
 Description: An exportation inference. (Contributed by NM, 26-Apr-1994.)
Hypothesis
Ref Expression
exp32.1 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
Assertion
Ref Expression
exp32 (𝜑 → (𝜓 → (𝜒𝜃)))

Proof of Theorem exp32
StepHypRef Expression
1 exp32.1 . . 3 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
21ex 112 . 2 (𝜑 → ((𝜓𝜒) → 𝜃))
32expd 249 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-ia3 105 This theorem is referenced by:  exp44  359  exp45  360  expr  361  anassrs  386  an13s  509  3impb  1111  xordidc  1306  funfvima3  5420  isoini  5485  ovg  5667  fundmen  6317  distrlem1prl  6738  distrlem1pru  6739  caucvgprprlemaddq  6864  recexgt0sr  6916  cnegexlem2  7250  mulgt1  7904  faclbnd  9609  oddpwdclemdvds  10258  oddpwdclemndvds  10259
 Copyright terms: Public domain W3C validator