![]() |
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 39842 3impexpbicomiVD 39854 tratrbVD 39857 idiVD 39860 ancomstVD 39861 ordelordALTVD 39863 equncomiVD 39865 sucidALTVD 39866 sucidVD 39868 ee33VD 39875 undif3VD 39878 onfrALTlem5VD 39881 onfrALTlem1VD 39886 onfrALTVD 39887 relopabVD 39897 19.41rgVD 39898 ax6e2ndVD 39904 2sb5ndVD 39906 sb5ALTVD 39909 vk15.4jVD 39910 |
Copyright terms: Public domain | W3C validator |