Theorem exp32 357

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 113	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
3	2	expd 254	1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Syntax hints:   → wi 4   ∧ wa 102

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

This theorem is referenced by:  exp44  365  exp45  366  expr  367  anassrs  392  an13s  531  3impb  1134  xordidc  1330  funfvima3  5413  isoini  5477  ovg  5659  fundmen  6309  distrlem1prl  6772  distrlem1pru  6773  caucvgprprlemaddq  6898  recexgt0sr  6950  cnegexlem2  7284  mulgt1  7941  faclbnd  9668  divgcdcoprm0  10483  cncongr2  10486  oddpwdclemdvds  10548  oddpwdclemndvds  10549