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  5561  funfvima3  5919  isoini  5990  ovg  6192  fundmen  7046  distrlem1prl  7896  distrlem1pru  7897  caucvgprprlemaddq  8022  recexgt0sr  8087  axpre-suploclemres  8215  cnegexlem2  8448  mulgt1  9136  faclbnd  11102  swrdwrdsymbg  11352  pfxccatin12lem2a  11415  pfxccat3  11422  swrdccat  11423  divgcdcoprm0  12794  cncongr2  12797  oddpwdclemdvds  12863  oddpwdclemndvds  12864  infpnlem1  13053  imasabl  14045  cnpnei  15076  dvmptfsum  15582  zabsle1  15864  lgsquad2lem2  15947  2lgsoddprm  15978  eupth2lemsfi  16465