Theorem expdcom 417

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  expd  418  odi  8197  nndi  8241  nnmass  8242  ttukeylem5  9927  genpnmax  10421  mulexp  13460  expadd  13463  expmul  13466  cshwidxmod  14157  prmgaplem6  16384  setsstruct  16515  usgredg2vlem2  27000  usgr2trlncl  27533  clwwlkel  27817  clwwlkf1  27820  wwlksext2clwwlk  27828  n4cyclfrgr  28062  5oalem6  29428  atom1d  30122  grpomndo  35145  pell14qrexpclnn0  39453  truniALT  40865  truniALTVD  41202  iccpartigtl  43573  sbgoldbm  43939  2zlidl  44195  rngccatidALTV  44250  ringccatidALTV  44313  nn0sumshdiglemA  44669