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  5567  funfvima3  5925  isoini  5997  ovg  6201  fundmen  7060  distrlem1prl  7913  distrlem1pru  7914  caucvgprprlemaddq  8039  recexgt0sr  8104  axpre-suploclemres  8232  cnegexlem2  8465  mulgt1  9154  faclbnd  11128  swrdwrdsymbg  11381  pfxccatin12lem2a  11444  pfxccat3  11451  swrdccat  11452  divgcdcoprm0  12823  cncongr2  12826  oddpwdclemdvds  12892  oddpwdclemndvds  12893  infpnlem1  13082  imasabl  14137  cnpnei  15196  dvmptfsum  15702  zabsle1  15984  lgsquad2lem2  16067  2lgsoddprm  16098  eupth2lemsfi  16585