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 40957 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 40916 | . . . 4 ⊢ (( 𝜑 ▶ 𝜓 ) → (𝜑 → 𝜓)) | |
3 | 1, 2 | ax-mp 5 | . . 3 ⊢ (𝜑 → 𝜓) |
4 | 3 | alrimiv 1928 | . 2 ⊢ (𝜑 → ∀𝑥𝜓) |
5 | dfvd1impr 40917 | . 2 ⊢ ((𝜑 → ∀𝑥𝜓) → ( 𝜑 ▶ ∀𝑥𝜓 )) | |
6 | 4, 5 | ax-mp 5 | 1 ⊢ ( 𝜑 ▶ ∀𝑥𝜓 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1535 ( wvd1 40910 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 |
This theorem depends on definitions: df-bi 209 df-vd1 40911 |
This theorem is referenced by: trsspwALT 41159 snssiALTVD 41168 sstrALT2VD 41175 elex2VD 41179 elex22VD 41180 tpid3gVD 41183 trsbcVD 41218 sbcssgVD 41224 csbingVD 41225 onfrALTVD 41232 csbsngVD 41234 csbxpgVD 41235 csbrngVD 41237 csbunigVD 41239 csbfv12gALTVD 41240 ax6e2eqVD 41248 ax6e2ndeqVD 41250 sspwimpVD 41260 sspwimpcfVD 41262 |
Copyright terms: Public domain | W3C validator |