![]() |
Mathbox for Alan Sare |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > e12 | Structured version Visualization version Unicode version |
Description: A virtual deduction elimination rule (see sylsyld 58). (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
e12.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
e12.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
e12.3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
e12 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | e12.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | vd12 36978 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | e12.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | e12.3 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 2, 3, 4 | e22 37049 |
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-an 377 df-vd1 36939 df-vd2 36947 |
This theorem is referenced by: e12an 37108 trsspwALT 37202 sspwtr 37205 pwtrVD 37216 snssiALTVD 37219 elex2VD 37230 elex22VD 37231 eqsbc3rVD 37232 en3lplem1VD 37235 3ornot23VD 37239 orbi1rVD 37240 19.21a3con13vVD 37244 exbirVD 37245 tratrbVD 37254 ssralv2VD 37259 sbcim2gVD 37268 sbcbiVD 37269 relopabVD 37294 19.41rgVD 37295 ax6e2eqVD 37300 ax6e2ndeqVD 37302 vk15.4jVD 37307 con3ALTVD 37309 |
Copyright terms: Public domain | W3C validator |