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  8591  nndi  8635  nnmass  8636  ttukeylem5  10527  genpnmax  11021  mulexp  14119  expadd  14122  expmul  14125  cshwidxmod  14821  prmgaplem6  17076  setsstruct  17195  usgredg2vlem2  29205  usgr2trlncl  29742  clwwlkel  30027  clwwlkf1  30030  wwlksext2clwwlk  30038  n4cyclfrgr  30272  5oalem6  31640  atom1d  32334  grpomndo  37899  pell14qrexpclnn0  42889  truniALT  44566  truniALTVD  44902  iccpartigtl  47437  sbgoldbm  47798  cycldlenngric  47941  2zlidl  48215  rngccatidALTV  48247  ringccatidALTV  48281  nn0sumshdiglemA  48599