Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  e0a Structured version   Visualization version   GIF version

Theorem e0a 44770
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.)
Hypotheses
Ref Expression
e0a.1 𝜑
e0a.2 (𝜑𝜓)
Assertion
Ref Expression
e0a 𝜓

Proof of Theorem e0a
StepHypRef Expression
1 e0a.1 . 2 𝜑
2 e0a.2 . 2 (𝜑𝜓)
31, 2ax-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