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 1934 is gen11 42204 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 42163 | . . . 4 ⊢ (( 𝜑 ▶ 𝜓 ) → (𝜑 → 𝜓)) | |
3 | 1, 2 | ax-mp 5 | . . 3 ⊢ (𝜑 → 𝜓) |
4 | 3 | alrimiv 1934 | . 2 ⊢ (𝜑 → ∀𝑥𝜓) |
5 | dfvd1impr 42164 | . 2 ⊢ ((𝜑 → ∀𝑥𝜓) → ( 𝜑 ▶ ∀𝑥𝜓 )) | |
6 | 4, 5 | ax-mp 5 | 1 ⊢ ( 𝜑 ▶ ∀𝑥𝜓 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1540 ( wvd1 42157 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 |
This theorem depends on definitions: df-bi 206 df-vd1 42158 |
This theorem is referenced by: trsspwALT 42406 snssiALTVD 42415 sstrALT2VD 42422 elex2VD 42426 elex22VD 42427 tpid3gVD 42430 trsbcVD 42465 sbcssgVD 42471 csbingVD 42472 onfrALTVD 42479 csbsngVD 42481 csbxpgVD 42482 csbrngVD 42484 csbunigVD 42486 csbfv12gALTVD 42487 ax6e2eqVD 42495 ax6e2ndeqVD 42497 sspwimpVD 42507 sspwimpcfVD 42509 |
Copyright terms: Public domain | W3C validator |