![]() |
Mathbox for Alan Sare |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > e10 | Structured version Visualization version Unicode version |
Description: A virtual deduction elimination rule (see mpisyl 21). (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
e10.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
e10.2 |
![]() ![]() |
e10.3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
e10 |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | e10.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | e10.2 |
. . 3
![]() ![]() | |
3 | 2 | vd01 36976 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
4 | e10.3 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 1, 3, 4 | e11 37067 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 189 df-vd1 36940 |
This theorem is referenced by: e10an 37074 en3lpVD 37241 3orbi123VD 37246 sbc3orgVD 37247 exbiriVD 37250 3impexpVD 37252 3impexpbicomVD 37253 al2imVD 37259 equncomVD 37265 trsbcVD 37274 sbcssgVD 37280 csbingVD 37281 onfrALTVD 37288 csbsngVD 37290 csbxpgVD 37291 csbresgVD 37292 csbrngVD 37293 csbima12gALTVD 37294 csbunigVD 37295 csbfv12gALTVD 37296 con5VD 37297 hbimpgVD 37301 hbalgVD 37302 hbexgVD 37303 ax6e2eqVD 37304 ax6e2ndeqVD 37306 e2ebindVD 37309 sb5ALTVD 37310 |
Copyright terms: Public domain | W3C validator |