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  8560  nndi  8605  nnmass  8606  ttukeylem5  10493  genpnmax  10988  mulexp  14133  expadd  14136  expmul  14139  cshwidxmod  14836  prmgaplem6  17112  setsstruct  17232  usgredg2vlem2  29513  usgr2trlncl  30046  clwwlkel  30334  clwwlkf1  30337  wwlksext2clwwlk  30345  n4cyclfrgr  30579  5oalem6  31948  atom1d  32642  grpomndo  38409  pell14qrexpclnn0  43478  truniALT  45135  truniALTVD  45471  iccpartigtl  48054  sbgoldbm  48431  cycldlenngric  48575  pgnbgreunbgrlem1  48760  pgnbgreunbgrlem2  48764  pgnbgreunbgrlem4  48766  pgnbgreunbgrlem5  48770  2zlidl  48887  rngccatidALTV  48919  ringccatidALTV  48953  nn0sumshdiglemA  49277