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  5540  funfvima3  5898  isoini  5969  ovg  6171  fundmen  7024  distrlem1prl  7845  distrlem1pru  7846  caucvgprprlemaddq  7971  recexgt0sr  8036  axpre-suploclemres  8164  cnegexlem2  8398  mulgt1  9086  faclbnd  11047  swrdwrdsymbg  11292  pfxccatin12lem2a  11355  pfxccat3  11362  swrdccat  11363  divgcdcoprm0  12734  cncongr2  12737  oddpwdclemdvds  12803  oddpwdclemndvds  12804  infpnlem1  12993  imasabl  13984  cnpnei  15010  dvmptfsum  15516  zabsle1  15798  lgsquad2lem2  15881  2lgsoddprm  15912  eupth2lemsfi  16399