Theorem expdcom 414

Description: Commuted form of expd 415. (Contributed by Alan Sare, 18-Mar-2012.) Shorten expd 415. (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 412	1 ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃)))

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  expd  415  odi  8543  nndi  8587  nnmass  8588  ttukeylem5  10466  genpnmax  10960  mulexp  14066  expadd  14069  expmul  14072  cshwidxmod  14768  prmgaplem6  17027  setsstruct  17146  usgredg2vlem2  29153  usgr2trlncl  29690  clwwlkel  29975  clwwlkf1  29978  wwlksext2clwwlk  29986  n4cyclfrgr  30220  5oalem6  31588  atom1d  32282  grpomndo  37869  pell14qrexpclnn0  42854  truniALT  44531  truniALTVD  44867  iccpartigtl  47424  sbgoldbm  47785  cycldlenngric  47928  pgnbgreunbgrlem1  48103  pgnbgreunbgrlem2  48107  pgnbgreunbgrlem4  48109  pgnbgreunbgrlem5  48113  2zlidl  48228  rngccatidALTV  48260  ringccatidALTV  48294  nn0sumshdiglemA  48608