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  1223  xordidc  1441  f0rn0  5516  funfvima3  5866  isoini  5935  ovg  6135  fundmen  6949  distrlem1prl  7757  distrlem1pru  7758  caucvgprprlemaddq  7883  recexgt0sr  7948  axpre-suploclemres  8076  cnegexlem2  8310  mulgt1  8998  faclbnd  10950  swrdwrdsymbg  11182  pfxccatin12lem2a  11245  pfxccat3  11252  swrdccat  11253  divgcdcoprm0  12609  cncongr2  12612  oddpwdclemdvds  12678  oddpwdclemndvds  12679  infpnlem1  12868  imasabl  13859  cnpnei  14878  dvmptfsum  15384  zabsle1  15663  lgsquad2lem2  15746  2lgsoddprm  15777