Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > exp4c | Structured version Visualization version Unicode version |
Description: An exportation inference. (Contributed by NM, 26-Apr-1994.) |
Ref | Expression |
---|---|
exp4c.1 |
Ref | Expression |
---|---|
exp4c |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exp4c.1 | . . 3 | |
2 | 1 | expd 452 | . 2 |
3 | 2 | expd 452 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 384 |
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 386 |
This theorem is referenced by: exp5j 645 oawordri 7630 oaordex 7638 odi 7659 pssnn 8178 alephval3 8933 dfac2 8953 axdc4lem 9277 leexp1a 12919 wrdsymb0 13339 swrdnd2 13433 coprmproddvds 15377 lmodvsmmulgdi 18898 assamulgscm 19350 2ndcctbss 21258 2pthnloop 26627 wwlksnext 26788 frgrregord013 27253 atcvatlem 29244 exp5g 32297 cdleme48gfv1 35824 cdlemg6e 35910 dihord5apre 36551 dihglblem5apreN 36580 iccpartgt 41363 lmodvsmdi 42163 lindslinindsimp1 42246 nn0sumshdiglemB 42414 |
Copyright terms: Public domain | W3C validator |