![]() |
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 44559 3impexpbicomiVD 44571 tratrbVD 44574 idiVD 44577 ancomstVD 44578 ordelordALTVD 44580 equncomiVD 44582 sucidALTVD 44583 sucidVD 44585 ee33VD 44592 undif3VD 44595 onfrALTlem5VD 44598 onfrALTlem1VD 44603 onfrALTVD 44604 relopabVD 44614 19.41rgVD 44615 ax6e2ndVD 44621 2sb5ndVD 44623 sb5ALTVD 44626 vk15.4jVD 44627 |
Copyright terms: Public domain | W3C validator |