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  8573  nndi  8618  nnmass  8619  ttukeylem5  10515  genpnmax  11010  mulexp  14157  expadd  14160  expmul  14163  cshwidxmod  14866  prmgaplem6  17141  setsstruct  17261  usgredg2vlem2  29613  usgr2trlncl  30146  clwwlkel  30434  clwwlkf1  30437  wwlksext2clwwlk  30445  n4cyclfrgr  30679  5oalem6  32048  atom1d  32742  grpomndo  38567  pell14qrexpclnn0  43634  truniALT  45291  truniALTVD  45627  iccpartigtl  48213  sbgoldbm  48590  cycldlenngric  48734  pgnbgreunbgrlem1  48919  pgnbgreunbgrlem2  48923  pgnbgreunbgrlem4  48925  pgnbgreunbgrlem5  48929  2zlidl  49046  rngccatidALTV  49078  ringccatidALTV  49112  nn0sumshdiglemA  49440