Mathbox for Alan Sare |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > e0a | Structured version Visualization version Unicode version |
Description: Elimination rule identical to ax-mp 5. The non-virtual deduction form is the virtual deduction form, which is ax-mp 5. (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
e0a.1 | |
e0a.2 |
Ref | Expression |
---|---|
e0a |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | e0a.1 | . 2 | |
2 | e0a.2 | . 2 | |
3 | 1, 2 | ax-mp 5 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 |
This theorem was proved from axioms: ax-mp 5 |
This theorem is referenced by: simplbi2VD 39081 3impexpbicomiVD 39093 tratrbVD 39097 idiVD 39100 ancomstVD 39101 ordelordALTVD 39103 equncomiVD 39105 sucidALTVD 39106 sucidVD 39108 ee33VD 39115 undif3VD 39118 onfrALTlem5VD 39121 onfrALTlem4VD 39122 onfrALTlem1VD 39126 onfrALTVD 39127 relopabVD 39137 19.41rgVD 39138 ax6e2ndVD 39144 2sb5ndVD 39146 sb5ALTVD 39149 vk15.4jVD 39150 |
Copyright terms: Public domain | W3C validator |