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  569  3impb  1226  xordidc  1444  f0rn0  5567  funfvima3  5925  isoini  5997  ovg  6201  fundmen  7060  distrlem1prl  7913  distrlem1pru  7914  caucvgprprlemaddq  8039  recexgt0sr  8104  axpre-suploclemres  8232  cnegexlem2  8466  mulgt1  9157  faclbnd  11131  swrdwrdsymbg  11384  pfxccatin12lem2a  11447  pfxccat3  11454  swrdccat  11455  divgcdcoprm0  12827  cncongr2  12830  oddpwdclemdvds  12896  oddpwdclemndvds  12897  infpnlem1  13086  imasabl  14093  cnpnei  15214  dvmptfsum  15720  zabsle1  16002  lgsquad2lem2  16085  2lgsoddprm  16116  eupth2lemsfi  16603