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  8570  nndi  8615  nnmass  8616  ttukeylem5  10519  genpnmax  11020  mulexp  14169  expadd  14172  expmul  14175  cshwidxmod  14878  prmgaplem6  17154  setsstruct  17274  usgredg2vlem2  29694  usgr2trlncl  30233  clwwlkel  30524  clwwlkf1  30527  wwlksext2clwwlk  30535  n4cyclfrgr  30779  5oalem6  32148  atom1d  32842  grpomndo  38633  pell14qrexpclnn0  43715  truniALT  45372  truniALTVD  45708  iccpartigtl  48331  sbgoldbm  48708  cycldlenngric  48852  pgnbgreunbgrlem1  49037  pgnbgreunbgrlem2  49041  pgnbgreunbgrlem4  49043  pgnbgreunbgrlem5  49047  2zlidl  49163  rngccatidALTV  49195  ringccatidALTV  49229  nn0sumshdiglemA  49557