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  8500  nndi  8544  nnmass  8545  ttukeylem5  10411  genpnmax  10905  mulexp  14010  expadd  14013  expmul  14016  cshwidxmod  14712  prmgaplem6  16970  setsstruct  17089  usgredg2vlem2  29206  usgr2trlncl  29740  clwwlkel  30028  clwwlkf1  30031  wwlksext2clwwlk  30039  n4cyclfrgr  30273  5oalem6  31641  atom1d  32335  grpomndo  37935  pell14qrexpclnn0  42983  truniALT  44658  truniALTVD  44994  iccpartigtl  47547  sbgoldbm  47908  cycldlenngric  48052  pgnbgreunbgrlem1  48237  pgnbgreunbgrlem2  48241  pgnbgreunbgrlem4  48243  pgnbgreunbgrlem5  48247  2zlidl  48364  rngccatidALTV  48396  ringccatidALTV  48430  nn0sumshdiglemA  48744