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 89	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 197  df-an 385

This theorem is referenced by:  odi  7704  nndi  7748  nnmass  7749  ttukeylem5  9373  genpnmax  9867  mulexp  12939  expadd  12942  expmul  12945  prmgaplem6  15807  setsstruct  15945  usgredg2vlem2  26163  usgr2trlncl  26712  clwwlkel  27009  clwwlkf1  27012  wwlksext2clwwlk  27021  n4cyclfrgr  27271  5oalem6  28646  atom1d  29340  grpomndo  33804  pell14qrexpclnn0  37747  truniALT  39068  truniALTVD  39428  iccpartigtl  41684  sbgoldbm  41997  2zlidl  42259  rngccatidALTV  42314  ringccatidALTV  42377  nn0sumshdiglemA  42738