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  404  an13s  573  3impb  1230  xordidc  1448  f0rn0  5585  funfvima3  5946  isoini  6018  ovg  6222  fundmen  7088  distrlem1prl  7943  distrlem1pru  7944  caucvgprprlemaddq  8069  recexgt0sr  8134  axpre-suploclemres  8262  cnegexlem2  8496  mulgt1  9187  faclbnd  11162  swrdwrdsymbg  11419  pfxccatin12lem2a  11482  pfxccat3  11489  swrdccat  11490  divgcdcoprm0  12862  cncongr2  12865  oddpwdclemdvds  12931  oddpwdclemndvds  12932  infpnlem1  13121  imasabl  14123  cnpnei  15303  dvmptfsum  15809  zabsle1  16101  lgsquad2lem2  16184  2lgsoddprm  16215  eupth2lemsfi  16702