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  8590  nndi  8635  nnmass  8636  ttukeylem5  10594  genpnmax  11095  mulexp  14247  expadd  14250  expmul  14253  cshwidxmod  14958  prmgaplem6  17239  setsstruct  17359  usgredg2vlem2  29812  usgr2trlncl  30351  clwwlkel  30642  clwwlkf1  30645  wwlksext2clwwlk  30653  n4cyclfrgr  30897  5oalem6  32266  atom1d  32960  grpomndo  38902  pell14qrexpclnn0  43966  truniALT  45617  truniALTVD  45953  iccpartigtl  48598  sbgoldbm  48975  cycldlenngric  49119  pgnbgreunbgrlem1  49304  pgnbgreunbgrlem2  49308  pgnbgreunbgrlem4  49310  pgnbgreunbgrlem5  49314  2zlidl  49430  rngccatidALTV  49462  ringccatidALTV  49496  nn0sumshdiglemA  49824