![]() |
Mathbox for Alan Sare |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > gen11 | Structured version Visualization version Unicode version |
Description: Virtual deduction generalizing rule for one quantifying variable and one virtual hypothesis. alrimiv 1783 is gen11 37037 without virtual deductions. (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
gen11.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
gen11 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | gen11.1 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | dfvd1imp 36987 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 5 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | alrimiv 1783 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | dfvd1impr 36988 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 4, 5 | ax-mp 5 |
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 ax-gen 1679 ax-4 1692 ax-5 1768 |
This theorem depends on definitions: df-bi 190 df-vd1 36982 |
This theorem is referenced by: trsspwALT 37245 snssiALTVD 37262 sstrALT2VD 37269 elex2VD 37273 elex22VD 37274 tpid3gVD 37277 trsbcVD 37313 sbcssgVD 37319 csbingVD 37320 onfrALTVD 37327 csbsngVD 37329 csbxpgVD 37330 csbrngVD 37332 csbunigVD 37334 csbfv12gALTVD 37335 ax6e2eqVD 37343 ax6e2ndeqVD 37345 sspwimpVD 37355 sspwimpcfVD 37357 |
Copyright terms: Public domain | W3C validator |