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

Theorem exp32 363
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 114 . 2 (𝜑 → ((𝜓𝜒) → 𝜃))
32expd 256 1 (𝜑 → (𝜓 → (𝜒𝜃)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107
This theorem is referenced by:  exp44  371  exp45  372  expr  373  anassrs  398  an13s  557  3impb  1181  xordidc  1381  f0rn0  5363  funfvima3  5697  isoini  5765  ovg  5956  fundmen  6748  distrlem1prl  7497  distrlem1pru  7498  caucvgprprlemaddq  7623  recexgt0sr  7688  axpre-suploclemres  7816  cnegexlem2  8046  mulgt1  8729  faclbnd  10610  divgcdcoprm0  11972  cncongr2  11975  oddpwdclemdvds  12039  oddpwdclemndvds  12040  cnpnei  12606
  Copyright terms: Public domain W3C validator