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 39524
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  39603  3impexpbicomiVD  39615  tratrbVD  39619  idiVD  39622  ancomstVD  39623  ordelordALTVD  39625  equncomiVD  39627  sucidALTVD  39628  sucidVD  39630  ee33VD  39637  undif3VD  39640  onfrALTlem5VD  39643  onfrALTlem4VD  39644  onfrALTlem1VD  39648  onfrALTVD  39649  relopabVD  39659  19.41rgVD  39660  ax6e2ndVD  39666  2sb5ndVD  39668  sb5ALTVD  39671  vk15.4jVD  39672
  Copyright terms: Public domain W3C validator