Theorem expdcom 418

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  expd  419  odi  8543  nndi  8588  nnmass  8589  ttukeylem5  10467  genpnmax  10962  mulexp  14111  expadd  14114  expmul  14117  cshwidxmod  14813  prmgaplem6  17075  setsstruct  17195  usgredg2vlem2  29373  usgr2trlncl  29906  clwwlkel  30194  clwwlkf1  30197  wwlksext2clwwlk  30205  n4cyclfrgr  30439  5oalem6  31808  atom1d  32502  grpomndo  38338  pell14qrexpclnn0  43407  truniALT  45081  truniALTVD  45417  iccpartigtl  47993  sbgoldbm  48370  cycldlenngric  48514  pgnbgreunbgrlem1  48699  pgnbgreunbgrlem2  48703  pgnbgreunbgrlem4  48705  pgnbgreunbgrlem5  48709  2zlidl  48826  rngccatidALTV  48858  ringccatidALTV  48892  nn0sumshdiglemA  49205