Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  expdcom Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 expd.1 . . 3 (𝜑 → ((𝜓𝜒) → 𝜃))
21com12 32 . 2 ((𝜓𝜒) → (𝜑𝜃))
32ex 416 1 (𝜓 → (𝜒 → (𝜑𝜃)))
 Colors of variables: wff setvar class 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 210  df-an 400 This theorem is referenced by:  expd  419  odi  8191  nndi  8235  nnmass  8236  ttukeylem5  9927  genpnmax  10421  mulexp  13467  expadd  13470  expmul  13473  cshwidxmod  14159  prmgaplem6  16385  setsstruct  16518  usgredg2vlem2  27026  usgr2trlncl  27559  clwwlkel  27841  clwwlkf1  27844  wwlksext2clwwlk  27852  n4cyclfrgr  28086  5oalem6  29452  atom1d  30146  grpomndo  35332  pell14qrexpclnn0  39850  truniALT  41290  truniALTVD  41627  iccpartigtl  43983  sbgoldbm  44345  2zlidl  44601  rngccatidALTV  44656  ringccatidALTV  44719  nn0sumshdiglemA  45074
 Copyright terms: Public domain W3C validator