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  5528  funfvima3  5883  isoini  5954  ovg  6156  fundmen  6976  distrlem1prl  7795  distrlem1pru  7796  caucvgprprlemaddq  7921  recexgt0sr  7986  axpre-suploclemres  8114  cnegexlem2  8348  mulgt1  9036  faclbnd  10996  swrdwrdsymbg  11238  pfxccatin12lem2a  11301  pfxccat3  11308  swrdccat  11309  divgcdcoprm0  12666  cncongr2  12669  oddpwdclemdvds  12735  oddpwdclemndvds  12736  infpnlem1  12925  imasabl  13916  cnpnei  14936  dvmptfsum  15442  zabsle1  15721  lgsquad2lem2  15804  2lgsoddprm  15835