Theorem expdcom 414

Description: Commuted form of expd 415. (Contributed by Alan Sare, 18-Mar-2012.) Shorten expd 415. (Revised by Wolf Lammen, 28-Jul-2022.)

Hypothesis

Ref	Expression
expd.1	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Assertion

Ref	Expression
expdcom	⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃)))

Proof of Theorem expdcom

Step	Hyp	Ref	Expression
1		expd.1	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
2	1	com12 32	. 2 ⊢ ((𝜓 ∧ 𝜒) → (𝜑 → 𝜃))
3	2	ex 412	1 ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃)))

Syntax hints:   → wi 4   ∧ wa 395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  expd  415  odi  8615  nndi  8659  nnmass  8660  ttukeylem5  10550  genpnmax  11044  mulexp  14138  expadd  14141  expmul  14144  cshwidxmod  14837  prmgaplem6  17089  setsstruct  17209  usgredg2vlem2  29257  usgr2trlncl  29792  clwwlkel  30074  clwwlkf1  30077  wwlksext2clwwlk  30085  n4cyclfrgr  30319  5oalem6  31687  atom1d  32381  grpomndo  37861  pell14qrexpclnn0  42853  truniALT  44538  truniALTVD  44875  iccpartigtl  47347  sbgoldbm  47708  2zlidl  48083  rngccatidALTV  48115  ringccatidALTV  48149  nn0sumshdiglemA  48468