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  1199  xordidc  1399  f0rn0  5412  funfvima3  5752  isoini  5821  ovg  6015  fundmen  6808  distrlem1prl  7583  distrlem1pru  7584  caucvgprprlemaddq  7709  recexgt0sr  7774  axpre-suploclemres  7902  cnegexlem2  8135  mulgt1  8822  faclbnd  10723  divgcdcoprm0  12103  cncongr2  12106  oddpwdclemdvds  12172  oddpwdclemndvds  12173  infpnlem1  12359  cnpnei  13804  zabsle1  14485