Theorem expdcom 419

Description: Commuted form of expd 420. (Contributed by Alan Sare, 18-Mar-2012.) Shorten expd 420. (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 33	. 2 ⊢ ((𝜓 ∧ 𝜒) → (𝜑 → 𝜃))
3	2	ex 417	1 ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃)))

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  expd  420  odi  8565  nndi  8610  nnmass  8611  ttukeylem5  10498  genpnmax  10993  mulexp  14139  expadd  14142  expmul  14145  cshwidxmod  14842  prmgaplem6  17117  setsstruct  17237  usgredg2vlem2  29554  usgr2trlncl  30087  clwwlkel  30375  clwwlkf1  30378  wwlksext2clwwlk  30386  n4cyclfrgr  30620  5oalem6  31989  atom1d  32683  grpomndo  38504  pell14qrexpclnn0  43573  truniALT  45230  truniALTVD  45566  iccpartigtl  48149  sbgoldbm  48526  cycldlenngric  48670  pgnbgreunbgrlem1  48855  pgnbgreunbgrlem2  48859  pgnbgreunbgrlem4  48861  pgnbgreunbgrlem5  48865  2zlidl  48982  rngccatidALTV  49014  ringccatidALTV  49048  nn0sumshdiglemA  49376