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 44485
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  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