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

Theorem exp4c 608
Description: An exportation inference. (Contributed by NM, 26-Apr-1994.)
Hypothesis
Ref Expression
exp4c.1
Assertion
Ref Expression
exp4c

Proof of Theorem exp4c
StepHypRef Expression
1 exp4c.1 . . 3
21expd 436 . 2
32expd 436 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  oawordri  7218  oaordex  7226  odi  7247  pssnn  7758  alephval3  8512  dfac2  8532  axdc4lem  8856  leexp1a  12224  wrdsymb0  12575  swrdvalodm2  12664  swrdvalodm  12665  lmodvsmmulgdi  17547  assamulgscm  17999  2ndcctbss  19956  wwlknext  24724  frgraregord013  25118  atcvatlem  27304  exp5g  30119  exp5j  30120  lmodvsmdi  32975  lindslinindsimp1  33058  cdleme48gfv1  36262  cdlemg6e  36348  dihord5apre  36989  dihglblem5apreN  37018
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 185  df-an 371
  Copyright terms: Public domain W3C validator