Theorem exp32 365

Description: An exportation inference. (Contributed by NM, 26-Apr-1994.)

Hypothesis

Ref	Expression
exp32.1	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Assertion

Ref	Expression
exp32	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Proof of Theorem exp32

Step	Hyp	Ref	Expression
1		exp32.1	. . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
2	1	ex 115	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
3	2	expd 258	1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  exp44  373  exp45  374  expr  375  anassrs  404  an13s  573  3impb  1230  xordidc  1448  f0rn0  5587  funfvima3  5952  isoini  6024  ovg  6228  fundmen  7094  distrlem1prl  7950  distrlem1pru  7951  caucvgprprlemaddq  8076  recexgt0sr  8141  axpre-suploclemres  8269  cnegexlem2  8504  mulgt1  9196  faclbnd  11194  swrdwrdsymbg  11451  pfxccatin12lem2a  11514  pfxccat3  11521  swrdccat  11522  divgcdcoprm0  12897  cncongr2  12900  nnmaxpwlemdvds  12967  nnmaxpwlemndvds  12968  infpnlem1  13160  imasabl  14191  cnpnei  15372  dvmptfsum  15878  zabsle1  16240  lgsquad2lem2  16323  2lgsoddprm  16354  eupth2lemsfi  16841