![]() |
Mathbox for Alan Sare |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > gen11 | Structured version Visualization version GIF version |
Description: Virtual deduction generalizing rule for one quantifying variable and one virtual hypothesis. alrimiv 1923 is gen11 44292 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 44251 | . . . 4 ⊢ (( 𝜑 ▶ 𝜓 ) → (𝜑 → 𝜓)) | |
3 | 1, 2 | ax-mp 5 | . . 3 ⊢ (𝜑 → 𝜓) |
4 | 3 | alrimiv 1923 | . 2 ⊢ (𝜑 → ∀𝑥𝜓) |
5 | dfvd1impr 44252 | . 2 ⊢ ((𝜑 → ∀𝑥𝜓) → ( 𝜑 ▶ ∀𝑥𝜓 )) | |
6 | 4, 5 | ax-mp 5 | 1 ⊢ ( 𝜑 ▶ ∀𝑥𝜓 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1532 ( wvd1 44245 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 |
This theorem depends on definitions: df-bi 206 df-vd1 44246 |
This theorem is referenced by: trsspwALT 44494 snssiALTVD 44503 sstrALT2VD 44510 elex2VD 44514 elex22VD 44515 tpid3gVD 44518 trsbcVD 44553 sbcssgVD 44559 csbingVD 44560 onfrALTVD 44567 csbsngVD 44569 csbxpgVD 44570 csbrngVD 44572 csbunigVD 44574 csbfv12gALTVD 44575 ax6e2eqVD 44583 ax6e2ndeqVD 44585 sspwimpVD 44595 sspwimpcfVD 44597 |
Copyright terms: Public domain | W3C validator |