Theorem expdcom 420

Description: Commuted form of expd 421. (Contributed by Alan Sare, 18-Mar-2012.) Shorten expd 421. (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 33	. 2 ⊢ ((𝜓 ∧ 𝜒) → (𝜑 → 𝜃))
3	2	ex 418	1 ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  expd  421  odi  8571  nndi  8616  nnmass  8617  ttukeylem5  10572  genpnmax  11073  mulexp  14224  expadd  14227  expmul  14230  cshwidxmod  14934  prmgaplem6  17214  setsstruct  17334  usgredg2vlem2  29789  usgr2trlncl  30328  clwwlkel  30619  clwwlkf1  30622  wwlksext2clwwlk  30630  n4cyclfrgr  30874  5oalem6  32243  atom1d  32937  grpomndo  38777  pell14qrexpclnn0  43826  truniALT  45483  truniALTVD  45819  iccpartigtl  48449  sbgoldbm  48826  cycldlenngric  48970  pgnbgreunbgrlem1  49155  pgnbgreunbgrlem2  49159  pgnbgreunbgrlem4  49161  pgnbgreunbgrlem5  49165  2zlidl  49281  rngccatidALTV  49313  ringccatidALTV  49347  nn0sumshdiglemA  49675