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  8617  nndi  8661  nnmass  8662  ttukeylem5  10553  genpnmax  11047  mulexp  14142  expadd  14145  expmul  14148  cshwidxmod  14841  prmgaplem6  17094  setsstruct  17213  usgredg2vlem2  29243  usgr2trlncl  29780  clwwlkel  30065  clwwlkf1  30068  wwlksext2clwwlk  30076  n4cyclfrgr  30310  5oalem6  31678  atom1d  32372  grpomndo  37882  pell14qrexpclnn0  42877  truniALT  44561  truniALTVD  44898  iccpartigtl  47410  sbgoldbm  47771  2zlidl  48156  rngccatidALTV  48188  ringccatidALTV  48222  nn0sumshdiglemA  48540