![]() |
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 44844 3impexpbicomiVD 44856 tratrbVD 44859 idiVD 44862 ancomstVD 44863 ordelordALTVD 44865 equncomiVD 44867 sucidALTVD 44868 sucidVD 44870 ee33VD 44877 undif3VD 44880 onfrALTlem5VD 44883 onfrALTlem1VD 44888 onfrALTVD 44889 relopabVD 44899 19.41rgVD 44900 ax6e2ndVD 44906 2sb5ndVD 44908 sb5ALTVD 44911 vk15.4jVD 44912 |
Copyright terms: Public domain | W3C validator |