| 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 1960 is gen11 45365 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 45324 | . . . 4 ⊢ (( 𝜑 ▶ 𝜓 ) → (𝜑 → 𝜓)) | |
| 3 | 1, 2 | ax-mp 5 | . . 3 ⊢ (𝜑 → 𝜓) |
| 4 | 3 | alrimiv 1960 | . 2 ⊢ (𝜑 → ∀𝑥𝜓) |
| 5 | dfvd1impr 45325 | . 2 ⊢ ((𝜑 → ∀𝑥𝜓) → ( 𝜑 ▶ ∀𝑥𝜓 )) | |
| 6 | 4, 5 | ax-mp 5 | 1 ⊢ ( 𝜑 ▶ ∀𝑥𝜓 ) |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: → wi 4 ∀wal 1568 ( wvd1 45318 |
| This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 |
| This proof depends on definitions: df-bi 210 df-vd1 45319 |
| This theorem is used by: trsspwALT 45566 snssiALTVD 45575 sstrALT2VD 45582 elex2VD 45586 elex22VD 45587 tpid3gVD 45590 trsbcVD 45625 sbcssgVD 45631 csbingVD 45632 onfrALTVD 45639 csbsngVD 45641 csbxpgVD 45642 csbrngVD 45644 csbunigVD 45646 csbfv12gALTVD 45647 ax6e2eqVD 45655 ax6e2ndeqVD 45657 sspwimpVD 45667 sspwimpcfVD 45669 |
| Copyright terms: Public domain | W3C validator |