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  8507  nndi  8552  nnmass  8553  ttukeylem5  10426  genpnmax  10921  mulexp  14054  expadd  14057  expmul  14060  cshwidxmod  14756  prmgaplem6  17018  setsstruct  17137  usgredg2vlem2  29309  usgr2trlncl  29843  clwwlkel  30131  clwwlkf1  30134  wwlksext2clwwlk  30142  n4cyclfrgr  30376  5oalem6  31745  atom1d  32439  grpomndo  38210  pell14qrexpclnn0  43312  truniALT  44986  truniALTVD  45322  iccpartigtl  47895  sbgoldbm  48272  cycldlenngric  48416  pgnbgreunbgrlem1  48601  pgnbgreunbgrlem2  48605  pgnbgreunbgrlem4  48607  pgnbgreunbgrlem5  48611  2zlidl  48728  rngccatidALTV  48760  ringccatidALTV  48794  nn0sumshdiglemA  49107