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 206  df-an 396

This theorem is referenced by:  expd  415  odi  8372  nndi  8416  nnmass  8417  ttukeylem5  10200  genpnmax  10694  mulexp  13750  expadd  13753  expmul  13756  cshwidxmod  14444  prmgaplem6  16685  setsstruct  16805  usgredg2vlem2  27496  usgr2trlncl  28029  clwwlkel  28311  clwwlkf1  28314  wwlksext2clwwlk  28322  n4cyclfrgr  28556  5oalem6  29922  atom1d  30616  grpomndo  35960  pell14qrexpclnn0  40604  truniALT  42050  truniALTVD  42387  iccpartigtl  44763  sbgoldbm  45124  2zlidl  45380  rngccatidALTV  45435  ringccatidALTV  45498  nn0sumshdiglemA  45853