|   | 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 44871 3impexpbicomiVD 44883 tratrbVD 44886 idiVD 44889 ancomstVD 44890 ordelordALTVD 44892 equncomiVD 44894 sucidALTVD 44895 sucidVD 44897 ee33VD 44904 undif3VD 44907 onfrALTlem5VD 44910 onfrALTlem1VD 44915 onfrALTVD 44916 relopabVD 44926 19.41rgVD 44927 ax6e2ndVD 44933 2sb5ndVD 44935 sb5ALTVD 44938 vk15.4jVD 44939 | 
| Copyright terms: Public domain | W3C validator |