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 87 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 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
 Copyright terms: Public domain W3C validator