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

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

Proof of Theorem exp44
StepHypRef Expression
1 exp44.1 . . 3
21exp32 605 . 2
32expd 436 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  wefrc  4878  tz7.7  4909  oalimcl  7228  unbenlem  14426  rnelfm  20454  wwlknimp  24687  spansncvi  26570  atom1d  27272  chirredlem3  27311  finminlem  30136  cvlcvr1  35064  lhpexle2lem  35733  trlord  36295  cdlemkid4  36660  dihord6apre  36983  dihglbcpreN  37027
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