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  8516  nndi  8561  nnmass  8562  ttukeylem5  10435  genpnmax  10930  mulexp  14036  expadd  14039  expmul  14042  cshwidxmod  14738  prmgaplem6  16996  setsstruct  17115  usgredg2vlem2  29311  usgr2trlncl  29845  clwwlkel  30133  clwwlkf1  30136  wwlksext2clwwlk  30144  n4cyclfrgr  30378  5oalem6  31746  atom1d  32440  grpomndo  38120  pell14qrexpclnn0  43217  truniALT  44891  truniALTVD  45227  iccpartigtl  47777  sbgoldbm  48138  cycldlenngric  48282  pgnbgreunbgrlem1  48467  pgnbgreunbgrlem2  48471  pgnbgreunbgrlem4  48473  pgnbgreunbgrlem5  48477  2zlidl  48594  rngccatidALTV  48626  ringccatidALTV  48660  nn0sumshdiglemA  48973