![]() |
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 1928 is gen11 41322 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 41281 | . . . 4 ⊢ (( 𝜑 ▶ 𝜓 ) → (𝜑 → 𝜓)) | |
3 | 1, 2 | ax-mp 5 | . . 3 ⊢ (𝜑 → 𝜓) |
4 | 3 | alrimiv 1928 | . 2 ⊢ (𝜑 → ∀𝑥𝜓) |
5 | dfvd1impr 41282 | . 2 ⊢ ((𝜑 → ∀𝑥𝜓) → ( 𝜑 ▶ ∀𝑥𝜓 )) | |
6 | 4, 5 | ax-mp 5 | 1 ⊢ ( 𝜑 ▶ ∀𝑥𝜓 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1536 ( wvd1 41275 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 |
This theorem depends on definitions: df-bi 210 df-vd1 41276 |
This theorem is referenced by: trsspwALT 41524 snssiALTVD 41533 sstrALT2VD 41540 elex2VD 41544 elex22VD 41545 tpid3gVD 41548 trsbcVD 41583 sbcssgVD 41589 csbingVD 41590 onfrALTVD 41597 csbsngVD 41599 csbxpgVD 41600 csbrngVD 41602 csbunigVD 41604 csbfv12gALTVD 41605 ax6e2eqVD 41613 ax6e2ndeqVD 41615 sspwimpVD 41625 sspwimpcfVD 41627 |
Copyright terms: Public domain | W3C validator |