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

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
StepHypRef Expression
1 expd.1 . . 3 (𝜑 → ((𝜓𝜒) → 𝜃))
21com12 32 . 2 ((𝜓𝜒) → (𝜑𝜃))
32ex 412 1 (𝜓 → (𝜒 → (𝜑𝜃)))
Colors of variables: wff setvar class
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  8617  nndi  8661  nnmass  8662  ttukeylem5  10553  genpnmax  11047  mulexp  14142  expadd  14145  expmul  14148  cshwidxmod  14841  prmgaplem6  17094  setsstruct  17213  usgredg2vlem2  29243  usgr2trlncl  29780  clwwlkel  30065  clwwlkf1  30068  wwlksext2clwwlk  30076  n4cyclfrgr  30310  5oalem6  31678  atom1d  32372  grpomndo  37882  pell14qrexpclnn0  42877  truniALT  44561  truniALTVD  44898  iccpartigtl  47410  sbgoldbm  47771  2zlidl  48156  rngccatidALTV  48188  ringccatidALTV  48222  nn0sumshdiglemA  48540
  Copyright terms: Public domain W3C validator