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  1199  xordidc  1399  f0rn0  5410  funfvima3  5750  isoini  5818  ovg  6012  fundmen  6805  distrlem1prl  7580  distrlem1pru  7581  caucvgprprlemaddq  7706  recexgt0sr  7771  axpre-suploclemres  7899  cnegexlem2  8131  mulgt1  8818  faclbnd  10716  divgcdcoprm0  12095  cncongr2  12098  oddpwdclemdvds  12164  oddpwdclemndvds  12165  infpnlem1  12351  cnpnei  13612  zabsle1  14293