Theorem expdcom 417

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  expd  418  odi  8207  nndi  8251  nnmass  8252  ttukeylem5  9937  genpnmax  10431  mulexp  13471  expadd  13474  expmul  13477  cshwidxmod  14167  prmgaplem6  16394  setsstruct  16525  usgredg2vlem2  27010  usgr2trlncl  27543  clwwlkel  27827  clwwlkf1  27830  wwlksext2clwwlk  27838  n4cyclfrgr  28072  5oalem6  29438  atom1d  30132  grpomndo  35155  pell14qrexpclnn0  39470  truniALT  40882  truniALTVD  41219  iccpartigtl  43590  sbgoldbm  43956  2zlidl  44212  rngccatidALTV  44267  ringccatidALTV  44330  nn0sumshdiglemA  44686