Theorem exp32 363

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

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  exp44  371  exp45  372  expr  373  anassrs  398  an13s  557  3impb  1178  xordidc  1378  f0rn0  5325  funfvima3  5659  isoini  5727  ovg  5917  fundmen  6708  distrlem1prl  7414  distrlem1pru  7415  caucvgprprlemaddq  7540  recexgt0sr  7605  axpre-suploclemres  7733  cnegexlem2  7962  mulgt1  8645  faclbnd  10519  divgcdcoprm0  11818  cncongr2  11821  oddpwdclemdvds  11884  oddpwdclemndvds  11885  cnpnei  12427