Theorem expdcom 420

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  expd  421  odi  8615  nndi  8660  nnmass  8661  ttukeylem5  10618  genpnmax  11119  mulexp  14271  expadd  14274  expmul  14277  cshwidxmod  14982  prmgaplem6  17263  setsstruct  17383  usgredg2vlem2  29837  usgr2trlncl  30376  clwwlkel  30667  clwwlkf1  30670  wwlksext2clwwlk  30678  n4cyclfrgr  30922  5oalem6  32291  atom1d  32985  grpomndo  39001  pell14qrexpclnn0  44066  truniALT  45715  truniALTVD  46051  iccpartigtl  48710  sbgoldbm  49087  cycldlenngric  49231  pgnbgreunbgrlem1  49416  pgnbgreunbgrlem2  49420  pgnbgreunbgrlem4  49422  pgnbgreunbgrlem5  49426  2zlidl  49542  rngccatidALTV  49574  ringccatidALTV  49608  nn0sumshdiglemA  49936