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  1202  xordidc  1419  f0rn0  5479  funfvima3  5828  isoini  5897  ovg  6095  fundmen  6909  distrlem1prl  7708  distrlem1pru  7709  caucvgprprlemaddq  7834  recexgt0sr  7899  axpre-suploclemres  8027  cnegexlem2  8261  mulgt1  8949  faclbnd  10899  swrdwrdsymbg  11131  divgcdcoprm0  12473  cncongr2  12476  oddpwdclemdvds  12542  oddpwdclemndvds  12543  infpnlem1  12732  imasabl  13722  cnpnei  14741  dvmptfsum  15247  zabsle1  15526  lgsquad2lem2  15609  2lgsoddprm  15640