![]() |
Mathbox for Alan Sare |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > e11 | Structured version Visualization version Unicode version |
Description: A virtual deduction elimination rule. (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
e11.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
e11.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
e11.3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
e11 |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | e11.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | e11.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | e11.3 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | a1i 11 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 1, 2, 4 | e111 37095 |
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 190 df-vd1 36982 |
This theorem is referenced by: e11an 37110 e01 37112 e10 37115 elex2VD 37273 elex22VD 37274 eqsbc3rVD 37275 tpid3gVD 37277 3ornot23VD 37282 orbi1rVD 37283 3orbi123VD 37285 sbc3orgVD 37286 sbcoreleleqVD 37295 ordelordALTVD 37303 sbcim2gVD 37311 trsbcVD 37313 undif3VD 37318 sbcssgVD 37319 csbingVD 37320 onfrALTVD 37327 csbeq2gVD 37328 csbsngVD 37329 csbxpgVD 37330 csbresgVD 37331 csbrngVD 37332 csbima12gALTVD 37333 csbunigVD 37334 csbfv12gALTVD 37335 19.41rgVD 37338 2pm13.193VD 37339 hbimpgVD 37340 ax6e2eqVD 37343 2uasbanhVD 37347 notnot2ALTVD 37351 |
Copyright terms: Public domain | W3C validator |