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 39768
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  39842  3impexpbicomiVD  39854  tratrbVD  39857  idiVD  39860  ancomstVD  39861  ordelordALTVD  39863  equncomiVD  39865  sucidALTVD  39866  sucidVD  39868  ee33VD  39875  undif3VD  39878  onfrALTlem5VD  39881  onfrALTlem1VD  39886  onfrALTVD  39887  relopabVD  39897  19.41rgVD  39898  ax6e2ndVD  39904  2sb5ndVD  39906  sb5ALTVD  39909  vk15.4jVD  39910
  Copyright terms: Public domain W3C validator