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

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
StepHypRef Expression
1 expdcom.1 . . 3 (𝜑 → ((𝜓𝜒) → 𝜃))
21expd 451 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32com3l 89 1 (𝜓 → (𝜒 → (𝜑𝜃)))
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator