Theorem expdcom 415

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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  expd  416  odi  8410  nndi  8454  nnmass  8455  ttukeylem5  10269  genpnmax  10763  mulexp  13822  expadd  13825  expmul  13828  cshwidxmod  14516  prmgaplem6  16757  setsstruct  16877  usgredg2vlem2  27593  usgr2trlncl  28128  clwwlkel  28410  clwwlkf1  28413  wwlksext2clwwlk  28421  n4cyclfrgr  28655  5oalem6  30021  atom1d  30715  grpomndo  36033  pell14qrexpclnn0  40688  truniALT  42161  truniALTVD  42498  iccpartigtl  44875  sbgoldbm  45236  2zlidl  45492  rngccatidALTV  45547  ringccatidALTV  45610  nn0sumshdiglemA  45965