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  8546  nndi  8590  nnmass  8591  ttukeylem5  10473  genpnmax  10967  mulexp  14073  expadd  14076  expmul  14079  cshwidxmod  14775  prmgaplem6  17034  setsstruct  17153  usgredg2vlem2  29160  usgr2trlncl  29697  clwwlkel  29982  clwwlkf1  29985  wwlksext2clwwlk  29993  n4cyclfrgr  30227  5oalem6  31595  atom1d  32289  grpomndo  37876  pell14qrexpclnn0  42861  truniALT  44538  truniALTVD  44874  iccpartigtl  47428  sbgoldbm  47789  cycldlenngric  47932  pgnbgreunbgrlem1  48107  pgnbgreunbgrlem2  48111  pgnbgreunbgrlem4  48113  pgnbgreunbgrlem5  48117  2zlidl  48232  rngccatidALTV  48264  ringccatidALTV  48298  nn0sumshdiglemA  48612