![]() |
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 40391 | . 2 ⊢ ( 𝜑 , 𝜒 ▶ 𝜓 ) |
3 | e12.2 | . 2 ⊢ ( 𝜑 , 𝜒 ▶ 𝜃 ) | |
4 | e12.3 | . 2 ⊢ (𝜓 → (𝜃 → 𝜏)) | |
5 | 2, 3, 4 | e22 40462 | 1 ⊢ ( 𝜑 , 𝜒 ▶ 𝜏 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ( wvd1 40360 ( wvd2 40368 |
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 199 df-an 388 df-vd1 40361 df-vd2 40369 |
This theorem is referenced by: e12an 40516 trsspwALT 40609 sspwtr 40612 pwtrVD 40615 snssiALTVD 40618 elex2VD 40629 elex22VD 40630 eqsbc3rVD 40631 en3lplem1VD 40634 3ornot23VD 40638 orbi1rVD 40639 19.21a3con13vVD 40643 exbirVD 40644 tratrbVD 40652 ssralv2VD 40657 sbcim2gVD 40666 sbcbiVD 40667 relopabVD 40692 19.41rgVD 40693 ax6e2eqVD 40698 ax6e2ndeqVD 40700 vk15.4jVD 40705 con3ALTVD 40707 |
Copyright terms: Public domain | W3C validator |