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  5525  funfvima3  5880  isoini  5951  ovg  6153  fundmen  6972  distrlem1prl  7785  distrlem1pru  7786  caucvgprprlemaddq  7911  recexgt0sr  7976  axpre-suploclemres  8104  cnegexlem2  8338  mulgt1  9026  faclbnd  10980  swrdwrdsymbg  11217  pfxccatin12lem2a  11280  pfxccat3  11287  swrdccat  11288  divgcdcoprm0  12644  cncongr2  12647  oddpwdclemdvds  12713  oddpwdclemndvds  12714  infpnlem1  12903  imasabl  13894  cnpnei  14914  dvmptfsum  15420  zabsle1  15699  lgsquad2lem2  15782  2lgsoddprm  15813