Theorem expdcom 413

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

Syntax hints:   → wi 4   ∧ wa 394

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 395

This theorem is referenced by:  expd  414  odi  8609  nndi  8653  nnmass  8654  ttukeylem5  10556  genpnmax  11050  mulexp  14121  expadd  14124  expmul  14127  cshwidxmod  14811  prmgaplem6  17058  setsstruct  17178  usgredg2vlem2  29162  usgr2trlncl  29697  clwwlkel  29979  clwwlkf1  29982  wwlksext2clwwlk  29990  n4cyclfrgr  30224  5oalem6  31592  atom1d  32286  grpomndo  37576  pell14qrexpclnn0  42523  truniALT  44217  truniALTVD  44554  iccpartigtl  46995  sbgoldbm  47356  2zlidl  47617  rngccatidALTV  47649  ringccatidALTV  47683  nn0sumshdiglemA  48007