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  8506  nndi  8551  nnmass  8552  ttukeylem5  10423  genpnmax  10918  mulexp  14024  expadd  14027  expmul  14030  cshwidxmod  14726  prmgaplem6  16984  setsstruct  17103  usgredg2vlem2  29299  usgr2trlncl  29833  clwwlkel  30121  clwwlkf1  30124  wwlksext2clwwlk  30132  n4cyclfrgr  30366  5oalem6  31734  atom1d  32428  grpomndo  38072  pell14qrexpclnn0  43104  truniALT  44778  truniALTVD  45114  iccpartigtl  47665  sbgoldbm  48026  cycldlenngric  48170  pgnbgreunbgrlem1  48355  pgnbgreunbgrlem2  48359  pgnbgreunbgrlem4  48361  pgnbgreunbgrlem5  48365  2zlidl  48482  rngccatidALTV  48514  ringccatidALTV  48548  nn0sumshdiglemA  48861