![]() |
Mathbox for Alan Sare |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > e0a | Structured version Visualization version GIF 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 39603 3impexpbicomiVD 39615 tratrbVD 39619 idiVD 39622 ancomstVD 39623 ordelordALTVD 39625 equncomiVD 39627 sucidALTVD 39628 sucidVD 39630 ee33VD 39637 undif3VD 39640 onfrALTlem5VD 39643 onfrALTlem4VD 39644 onfrALTlem1VD 39648 onfrALTVD 39649 relopabVD 39659 19.41rgVD 39660 ax6e2ndVD 39666 2sb5ndVD 39668 sb5ALTVD 39671 vk15.4jVD 39672 |
Copyright terms: Public domain | W3C validator |