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  1201  xordidc  1410  f0rn0  5448  funfvima3  5792  isoini  5861  ovg  6057  fundmen  6860  distrlem1prl  7642  distrlem1pru  7643  caucvgprprlemaddq  7768  recexgt0sr  7833  axpre-suploclemres  7961  cnegexlem2  8195  mulgt1  8882  faclbnd  10812  divgcdcoprm0  12239  cncongr2  12242  oddpwdclemdvds  12308  oddpwdclemndvds  12309  infpnlem1  12497  imasabl  13406  cnpnei  14387  zabsle1  15115