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  5522  funfvima3  5877  isoini  5948  ovg  6150  fundmen  6967  distrlem1prl  7777  distrlem1pru  7778  caucvgprprlemaddq  7903  recexgt0sr  7968  axpre-suploclemres  8096  cnegexlem2  8330  mulgt1  9018  faclbnd  10971  swrdwrdsymbg  11204  pfxccatin12lem2a  11267  pfxccat3  11274  swrdccat  11275  divgcdcoprm0  12631  cncongr2  12634  oddpwdclemdvds  12700  oddpwdclemndvds  12701  infpnlem1  12890  imasabl  13881  cnpnei  14901  dvmptfsum  15407  zabsle1  15686  lgsquad2lem2  15769  2lgsoddprm  15800