| 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 1927 is gen11 44636 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 44595 | . . . 4 ⊢ (( 𝜑 ▶ 𝜓 ) → (𝜑 → 𝜓)) | |
| 3 | 1, 2 | ax-mp 5 | . . 3 ⊢ (𝜑 → 𝜓) |
| 4 | 3 | alrimiv 1927 | . 2 ⊢ (𝜑 → ∀𝑥𝜓) |
| 5 | dfvd1impr 44596 | . 2 ⊢ ((𝜑 → ∀𝑥𝜓) → ( 𝜑 ▶ ∀𝑥𝜓 )) | |
| 6 | 4, 5 | ax-mp 5 | 1 ⊢ ( 𝜑 ▶ ∀𝑥𝜓 ) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∀wal 1538 ( wvd1 44589 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 |
| This theorem depends on definitions: df-bi 207 df-vd1 44590 |
| This theorem is referenced by: trsspwALT 44838 snssiALTVD 44847 sstrALT2VD 44854 elex2VD 44858 elex22VD 44859 tpid3gVD 44862 trsbcVD 44897 sbcssgVD 44903 csbingVD 44904 onfrALTVD 44911 csbsngVD 44913 csbxpgVD 44914 csbrngVD 44916 csbunigVD 44918 csbfv12gALTVD 44919 ax6e2eqVD 44927 ax6e2ndeqVD 44929 sspwimpVD 44939 sspwimpcfVD 44941 |
| Copyright terms: Public domain | W3C validator |