Theorem expdcom 415

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  expd  416  odi  8511  nndi  8556  nnmass  8557  ttukeylem5  10433  genpnmax  10928  mulexp  14061  expadd  14064  expmul  14067  cshwidxmod  14763  prmgaplem6  17025  setsstruct  17144  usgredg2vlem2  29320  usgr2trlncl  29853  clwwlkel  30141  clwwlkf1  30144  wwlksext2clwwlk  30152  n4cyclfrgr  30386  5oalem6  31755  atom1d  32449  grpomndo  38249  pell14qrexpclnn0  43318  truniALT  44992  truniALTVD  45328  iccpartigtl  47905  sbgoldbm  48282  cycldlenngric  48426  pgnbgreunbgrlem1  48611  pgnbgreunbgrlem2  48615  pgnbgreunbgrlem4  48617  pgnbgreunbgrlem5  48621  2zlidl  48738  rngccatidALTV  48770  ringccatidALTV  48804  nn0sumshdiglemA  49117