![]() |
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 1925 is gen11 44614 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 44573 | . . . 4 ⊢ (( 𝜑 ▶ 𝜓 ) → (𝜑 → 𝜓)) | |
3 | 1, 2 | ax-mp 5 | . . 3 ⊢ (𝜑 → 𝜓) |
4 | 3 | alrimiv 1925 | . 2 ⊢ (𝜑 → ∀𝑥𝜓) |
5 | dfvd1impr 44574 | . 2 ⊢ ((𝜑 → ∀𝑥𝜓) → ( 𝜑 ▶ ∀𝑥𝜓 )) | |
6 | 4, 5 | ax-mp 5 | 1 ⊢ ( 𝜑 ▶ ∀𝑥𝜓 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1535 ( wvd1 44567 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 |
This theorem depends on definitions: df-bi 207 df-vd1 44568 |
This theorem is referenced by: trsspwALT 44816 snssiALTVD 44825 sstrALT2VD 44832 elex2VD 44836 elex22VD 44837 tpid3gVD 44840 trsbcVD 44875 sbcssgVD 44881 csbingVD 44882 onfrALTVD 44889 csbsngVD 44891 csbxpgVD 44892 csbrngVD 44894 csbunigVD 44896 csbfv12gALTVD 44897 ax6e2eqVD 44905 ax6e2ndeqVD 44907 sspwimpVD 44917 sspwimpcfVD 44919 |
Copyright terms: Public domain | W3C validator |