MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  exp3acom3r Unicode version

Theorem exp3acom3r 1406
Description: Export and commute antecedents. (Contributed by Alan Sare, 18-Mar-2012.)
Hypothesis
Ref Expression
exp3acom3r.1
Assertion
Ref Expression
exp3acom3r

Proof of Theorem exp3acom3r
StepHypRef Expression
1 exp3acom3r.1 . . 3
21exp3a 429 . 2
32com3l 78 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 362
This theorem is referenced by:  odi  6979  nndi  7023  nnmass  7024  ttukeylem5  8629  genpnmax  9122  mulexp  11844  expadd  11847  expmul  11850  usgraidx2vlem2  22989  grpomndo  23512  5oalem6  24741  atom1d  25436  pell14qrexpclnn0  28880  usg2wlkonot  30076  clwwlkel  30129  clwwlkf1  30132  erclwwlktr  30159  erclwwlkntr  30175  usg2spot2nb  30332  truniALT  30825  truniALTVD  31192
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 179  df-an 364
  Copyright terms: Public domain W3C validator