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  8552  nndi  8597  nnmass  8598  ttukeylem5  10485  genpnmax  10980  mulexp  14128  expadd  14131  expmul  14134  cshwidxmod  14830  prmgaplem6  17106  setsstruct  17226  usgredg2vlem2  29485  usgr2trlncl  30018  clwwlkel  30306  clwwlkf1  30309  wwlksext2clwwlk  30317  n4cyclfrgr  30551  5oalem6  31920  atom1d  32614  grpomndo  38386  pell14qrexpclnn0  43455  truniALT  45115  truniALTVD  45451  iccpartigtl  48027  sbgoldbm  48404  cycldlenngric  48548  pgnbgreunbgrlem1  48733  pgnbgreunbgrlem2  48737  pgnbgreunbgrlem4  48739  pgnbgreunbgrlem5  48743  2zlidl  48860  rngccatidALTV  48892  ringccatidALTV  48926  nn0sumshdiglemA  49250