![]() |
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 2026 is gen11 39662 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 39612 | . . . 4 ⊢ (( 𝜑 ▶ 𝜓 ) → (𝜑 → 𝜓)) | |
3 | 1, 2 | ax-mp 5 | . . 3 ⊢ (𝜑 → 𝜓) |
4 | 3 | alrimiv 2026 | . 2 ⊢ (𝜑 → ∀𝑥𝜓) |
5 | dfvd1impr 39613 | . 2 ⊢ ((𝜑 → ∀𝑥𝜓) → ( 𝜑 ▶ ∀𝑥𝜓 )) | |
6 | 4, 5 | ax-mp 5 | 1 ⊢ ( 𝜑 ▶ ∀𝑥𝜓 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1654 ( wvd1 39606 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 |
This theorem depends on definitions: df-bi 199 df-vd1 39607 |
This theorem is referenced by: trsspwALT 39865 snssiALTVD 39874 sstrALT2VD 39881 elex2VD 39885 elex22VD 39886 tpid3gVD 39889 trsbcVD 39924 sbcssgVD 39930 csbingVD 39931 onfrALTVD 39938 csbsngVD 39940 csbxpgVD 39941 csbrngVD 39943 csbunigVD 39945 csbfv12gALTVD 39946 ax6e2eqVD 39954 ax6e2ndeqVD 39956 sspwimpVD 39966 sspwimpcfVD 39968 |
Copyright terms: Public domain | W3C validator |