Theorem exp32 358

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

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  exp44  366  exp45  367  expr  368  anassrs  393  an13s  535  3impb  1140  xordidc  1336  f0rn0  5220  funfvima3  5544  isoini  5613  ovg  5799  fundmen  6579  distrlem1prl  7204  distrlem1pru  7205  caucvgprprlemaddq  7330  recexgt0sr  7382  cnegexlem2  7721  mulgt1  8387  faclbnd  10212  divgcdcoprm0  11424  cncongr2  11427  oddpwdclemdvds  11489  oddpwdclemndvds  11490