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 41261
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  41335  3impexpbicomiVD  41347  tratrbVD  41350  idiVD  41353  ancomstVD  41354  ordelordALTVD  41356  equncomiVD  41358  sucidALTVD  41359  sucidVD  41361  ee33VD  41368  undif3VD  41371  onfrALTlem5VD  41374  onfrALTlem1VD  41379  onfrALTVD  41380  relopabVD  41390  19.41rgVD  41391  ax6e2ndVD  41397  2sb5ndVD  41399  sb5ALTVD  41402  vk15.4jVD  41403
  Copyright terms: Public domain W3C validator