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 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is referenced by:  exp44  373  exp45  374  expr  375  anassrs  400  an13s  567  3impb  1223  xordidc  1441  f0rn0  5526  funfvima3  5881  isoini  5952  ovg  6154  fundmen  6974  distrlem1prl  7790  distrlem1pru  7791  caucvgprprlemaddq  7916  recexgt0sr  7981  axpre-suploclemres  8109  cnegexlem2  8343  mulgt1  9031  faclbnd  10991  swrdwrdsymbg  11232  pfxccatin12lem2a  11295  pfxccat3  11302  swrdccat  11303  divgcdcoprm0  12660  cncongr2  12663  oddpwdclemdvds  12729  oddpwdclemndvds  12730  infpnlem1  12919  imasabl  13910  cnpnei  14930  dvmptfsum  15436  zabsle1  15715  lgsquad2lem2  15798  2lgsoddprm  15829