Theorem expdcom 413

Description: Commuted form of expd 414. (Contributed by Alan Sare, 18-Mar-2012.) Shorten expd 414. (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 411	1 ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃)))

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  expd  414  odi  8581  nndi  8625  nnmass  8626  ttukeylem5  10510  genpnmax  11004  mulexp  14071  expadd  14074  expmul  14077  cshwidxmod  14757  prmgaplem6  16993  setsstruct  17113  usgredg2vlem2  28750  usgr2trlncl  29284  clwwlkel  29566  clwwlkf1  29569  wwlksext2clwwlk  29577  n4cyclfrgr  29811  5oalem6  31179  atom1d  31873  grpomndo  37046  pell14qrexpclnn0  41906  truniALT  43604  truniALTVD  43941  iccpartigtl  46389  sbgoldbm  46750  2zlidl  46920  rngccatidALTV  46975  ringccatidALTV  47038  nn0sumshdiglemA  47392