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  8514  nndi  8559  nnmass  8560  ttukeylem5  10435  genpnmax  10930  mulexp  14063  expadd  14066  expmul  14069  cshwidxmod  14765  prmgaplem6  17027  setsstruct  17146  usgredg2vlem2  29295  usgr2trlncl  29828  clwwlkel  30116  clwwlkf1  30119  wwlksext2clwwlk  30127  n4cyclfrgr  30361  5oalem6  31730  atom1d  32424  grpomndo  38196  pell14qrexpclnn0  43294  truniALT  44968  truniALTVD  45304  iccpartigtl  47883  sbgoldbm  48260  cycldlenngric  48404  pgnbgreunbgrlem1  48589  pgnbgreunbgrlem2  48593  pgnbgreunbgrlem4  48595  pgnbgreunbgrlem5  48599  2zlidl  48716  rngccatidALTV  48748  ringccatidALTV  48782  nn0sumshdiglemA  49095