Theorem expdcom 454

Description: Commuted form of expd 451. (Contributed by Alan Sare, 18-Mar-2012.)

Hypothesis

Ref	Expression
expdcom.1	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Assertion

Ref	Expression
expdcom	⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃)))

Proof of Theorem expdcom

Step	Hyp	Ref	Expression
1		expdcom.1	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
2	1	expd 451	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	com3l 87	1 ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃)))

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  odi  7546  nndi  7590  nnmass  7591  ttukeylem5  9218  genpnmax  9708  mulexp  12761  expadd  12764  expmul  12767  prmgaplem6  15598  usgraidx2vlem2  25921  clwwlkel  26321  clwwlkf1  26324  erclwwlktr  26343  erclwwlkntr  26355  usg2wlkonot  26410  usg2spot2nb  26592  5oalem6  27902  atom1d  28596  grpomndo  32844  pell14qrexpclnn0  36448  truniALT  37772  truniALTVD  38136  iccpartigtl  39961  usgredg2vlem2  40453  clwwlksel  41221  clwwlksf1  41224  n4cyclfrgr  41461  2zlidl  41724  rngccatidALTV  41781  ringccatidALTV  41844  nn0sumshdiglemA  42211