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  5590  funfvima3  5955  isoini  6027  ovg  6231  fundmen  7099  distrlem1prl  7956  distrlem1pru  7957  caucvgprprlemaddq  8082  recexgt0sr  8147  axpre-suploclemres  8275  cnegexlem2  8510  mulgt1  9202  faclbnd  11202  swrdwrdsymbg  11459  pfxccatin12lem2a  11522  pfxccat3  11529  swrdccat  11530  divgcdcoprm0  12905  cncongr2  12908  nnmaxpwlemdvds  12975  nnmaxpwlemndvds  12976  infpnlem1  13168  imasabl  14231  cnpnei  15457  dvmptfsum  15963  zabsle1  16335  lgsquad2lem2  16418  2lgsoddprm  16449  eupth2lemsfi  16936