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  8504  nndi  8548  nnmass  8549  ttukeylem5  10426  genpnmax  10920  mulexp  14026  expadd  14029  expmul  14032  cshwidxmod  14727  prmgaplem6  16986  setsstruct  17105  usgredg2vlem2  29189  usgr2trlncl  29723  clwwlkel  30008  clwwlkf1  30011  wwlksext2clwwlk  30019  n4cyclfrgr  30253  5oalem6  31621  atom1d  32315  grpomndo  37854  pell14qrexpclnn0  42839  truniALT  44515  truniALTVD  44851  iccpartigtl  47408  sbgoldbm  47769  cycldlenngric  47913  pgnbgreunbgrlem1  48098  pgnbgreunbgrlem2  48102  pgnbgreunbgrlem4  48104  pgnbgreunbgrlem5  48108  2zlidl  48225  rngccatidALTV  48257  ringccatidALTV  48291  nn0sumshdiglemA  48605