Theorem expdcom 418

Description: Commuted form of expd 419. (Contributed by Alan Sare, 18-Mar-2012.) Shorten expd 419. (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 32	. 2 ⊢ ((𝜓 ∧ 𝜒) → (𝜑 → 𝜃))
3	2	ex 416	1 ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃)))

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  expd  419  odi  8307  nndi  8351  nnmass  8352  ttukeylem5  10127  genpnmax  10621  mulexp  13674  expadd  13677  expmul  13680  cshwidxmod  14368  prmgaplem6  16609  setsstruct  16729  usgredg2vlem2  27314  usgr2trlncl  27847  clwwlkel  28129  clwwlkf1  28132  wwlksext2clwwlk  28140  n4cyclfrgr  28374  5oalem6  29740  atom1d  30434  grpomndo  35770  pell14qrexpclnn0  40391  truniALT  41834  truniALTVD  42171  iccpartigtl  44548  sbgoldbm  44909  2zlidl  45165  rngccatidALTV  45220  ringccatidALTV  45283  nn0sumshdiglemA  45638