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

Theorem expdcom 415
Description: Commuted form of expd 416. (Contributed by Alan Sare, 18-Mar-2012.) Shorten expd 416. (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 413 1 (𝜓 → (𝜒 → (𝜑𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 206  df-an 397
This theorem is referenced by:  expd  416  odi  8523  nndi  8567  nnmass  8568  ttukeylem5  10446  genpnmax  10940  mulexp  14004  expadd  14007  expmul  14010  cshwidxmod  14688  prmgaplem6  16925  setsstruct  17045  usgredg2vlem2  28072  usgr2trlncl  28606  clwwlkel  28888  clwwlkf1  28891  wwlksext2clwwlk  28899  n4cyclfrgr  29133  5oalem6  30499  atom1d  31193  grpomndo  36323  pell14qrexpclnn0  41165  truniALT  42803  truniALTVD  43140  iccpartigtl  45585  sbgoldbm  45946  2zlidl  46202  rngccatidALTV  46257  ringccatidALTV  46320  nn0sumshdiglemA  46675
  Copyright terms: Public domain W3C validator