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  1201  xordidc  1410  f0rn0  5455  funfvima3  5799  isoini  5868  ovg  6066  fundmen  6874  distrlem1prl  7668  distrlem1pru  7669  caucvgprprlemaddq  7794  recexgt0sr  7859  axpre-suploclemres  7987  cnegexlem2  8221  mulgt1  8909  faclbnd  10852  divgcdcoprm0  12296  cncongr2  12299  oddpwdclemdvds  12365  oddpwdclemndvds  12366  infpnlem1  12555  imasabl  13544  cnpnei  14563  dvmptfsum  15069  zabsle1  15348  lgsquad2lem2  15431  2lgsoddprm  15462