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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  exp44  373  exp45  374  expr  375  anassrs  404  an13s  573  3impb  1230  xordidc  1448  f0rn0  5587  funfvima3  5952  isoini  6024  ovg  6228  fundmen  7094  distrlem1prl  7949  distrlem1pru  7950  caucvgprprlemaddq  8075  recexgt0sr  8140  axpre-suploclemres  8268  cnegexlem2  8502  mulgt1  9194  faclbnd  11181  swrdwrdsymbg  11438  pfxccatin12lem2a  11501  pfxccat3  11508  swrdccat  11509  divgcdcoprm0  12881  cncongr2  12884  oddpwdclemdvds  12950  oddpwdclemndvds  12951  infpnlem1  13140  imasabl  14142  cnpnei  15322  dvmptfsum  15828  zabsle1  16130  lgsquad2lem2  16213  2lgsoddprm  16244  eupth2lemsfi  16731