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

Theorem expdcom 455
 Description: Commuted form of expd 452. (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 452 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32com3l 89 1 (𝜓 → (𝜒 → (𝜑𝜃)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384 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 386 This theorem is referenced by:  odi  7611  nndi  7655  nnmass  7656  ttukeylem5  9286  genpnmax  9780  mulexp  12846  expadd  12849  expmul  12852  prmgaplem6  15691  setsstruct  15826  usgredg2vlem2  26024  usgr2trlncl  26538  clwwlksel  26793  clwwlksf1  26796  n4cyclfrgr  27032  5oalem6  28385  atom1d  29079  grpomndo  33333  pell14qrexpclnn0  36937  truniALT  38260  truniALTVD  38624  iccpartigtl  40678  2zlidl  41243  rngccatidALTV  41298  ringccatidALTV  41361  nn0sumshdiglemA  41726
 Copyright terms: Public domain W3C validator