![]() |
Mathbox for Alan Sare |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > e12 | Structured version Visualization version GIF version |
Description: A virtual deduction elimination rule (see sylsyld 61). (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
e12.1 | ⊢ ( 𝜑 ▶ 𝜓 ) |
e12.2 | ⊢ ( 𝜑 , 𝜒 ▶ 𝜃 ) |
e12.3 | ⊢ (𝜓 → (𝜃 → 𝜏)) |
Ref | Expression |
---|---|
e12 | ⊢ ( 𝜑 , 𝜒 ▶ 𝜏 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | e12.1 | . . 3 ⊢ ( 𝜑 ▶ 𝜓 ) | |
2 | 1 | vd12 43346 | . 2 ⊢ ( 𝜑 , 𝜒 ▶ 𝜓 ) |
3 | e12.2 | . 2 ⊢ ( 𝜑 , 𝜒 ▶ 𝜃 ) | |
4 | e12.3 | . 2 ⊢ (𝜓 → (𝜃 → 𝜏)) | |
5 | 2, 3, 4 | e22 43417 | 1 ⊢ ( 𝜑 , 𝜒 ▶ 𝜏 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ( wvd1 43315 ( wvd2 43323 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 206 df-an 397 df-vd1 43316 df-vd2 43324 |
This theorem is referenced by: e12an 43471 trsspwALT 43564 sspwtr 43567 pwtrVD 43570 snssiALTVD 43573 elex2VD 43584 elex22VD 43585 eqsbc2VD 43586 en3lplem1VD 43589 3ornot23VD 43593 orbi1rVD 43594 19.21a3con13vVD 43598 exbirVD 43599 tratrbVD 43607 ssralv2VD 43612 sbcim2gVD 43621 sbcbiVD 43622 relopabVD 43647 19.41rgVD 43648 ax6e2eqVD 43653 ax6e2ndeqVD 43655 vk15.4jVD 43660 con3ALTVD 43662 |
Copyright terms: Public domain | W3C validator |