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

Theorem expdcom 399
Description: Commuted form of expd 400. (Contributed by Alan Sare, 18-Mar-2012.) Shorten expd 400. (Revised, 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 397 1 (𝜓 → (𝜒 → (𝜑𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 383
This theorem is referenced by:  expd  400  odi  7813  nndi  7857  nnmass  7858  ttukeylem5  9537  genpnmax  10031  mulexp  13106  expadd  13109  expmul  13112  prmgaplem6  15967  setsstruct  16105  usgredg2vlem2  26340  usgr2trlncl  26891  clwwlkel  27202  clwwlkf1  27205  wwlksext2clwwlk  27214  n4cyclfrgr  27473  5oalem6  28858  atom1d  29552  grpomndo  34006  pell14qrexpclnn0  37956  truniALT  39276  truniALTVD  39636  iccpartigtl  41887  sbgoldbm  42200  2zlidl  42462  rngccatidALTV  42517  ringccatidALTV  42580  nn0sumshdiglemA  42941
  Copyright terms: Public domain W3C validator