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  1225  xordidc  1443  f0rn0  5531  funfvima3  5888  isoini  5959  ovg  6161  fundmen  6981  distrlem1prl  7802  distrlem1pru  7803  caucvgprprlemaddq  7928  recexgt0sr  7993  axpre-suploclemres  8121  cnegexlem2  8355  mulgt1  9043  faclbnd  11004  swrdwrdsymbg  11249  pfxccatin12lem2a  11312  pfxccat3  11319  swrdccat  11320  divgcdcoprm0  12678  cncongr2  12681  oddpwdclemdvds  12747  oddpwdclemndvds  12748  infpnlem1  12937  imasabl  13928  cnpnei  14949  dvmptfsum  15455  zabsle1  15734  lgsquad2lem2  15817  2lgsoddprm  15848  eupth2lemsfi  16335