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  8494  nndi  8538  nnmass  8539  ttukeylem5  10401  genpnmax  10895  mulexp  14005  expadd  14008  expmul  14011  cshwidxmod  14707  prmgaplem6  16965  setsstruct  17084  usgredg2vlem2  29202  usgr2trlncl  29736  clwwlkel  30021  clwwlkf1  30024  wwlksext2clwwlk  30032  n4cyclfrgr  30266  5oalem6  31634  atom1d  32328  grpomndo  37914  pell14qrexpclnn0  42898  truniALT  44573  truniALTVD  44909  iccpartigtl  47453  sbgoldbm  47814  cycldlenngric  47958  pgnbgreunbgrlem1  48143  pgnbgreunbgrlem2  48147  pgnbgreunbgrlem4  48149  pgnbgreunbgrlem5  48153  2zlidl  48270  rngccatidALTV  48302  ringccatidALTV  48336  nn0sumshdiglemA  48650