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 40811 | . 2 ⊢ ( 𝜑 , 𝜒 ▶ 𝜓 ) |
3 | e12.2 | . 2 ⊢ ( 𝜑 , 𝜒 ▶ 𝜃 ) | |
4 | e12.3 | . 2 ⊢ (𝜓 → (𝜃 → 𝜏)) | |
5 | 2, 3, 4 | e22 40882 | 1 ⊢ ( 𝜑 , 𝜒 ▶ 𝜏 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ( wvd1 40780 ( wvd2 40788 |
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 208 df-an 397 df-vd1 40781 df-vd2 40789 |
This theorem is referenced by: e12an 40936 trsspwALT 41029 sspwtr 41032 pwtrVD 41035 snssiALTVD 41038 elex2VD 41049 elex22VD 41050 eqsbc3rVD 41051 en3lplem1VD 41054 3ornot23VD 41058 orbi1rVD 41059 19.21a3con13vVD 41063 exbirVD 41064 tratrbVD 41072 ssralv2VD 41077 sbcim2gVD 41086 sbcbiVD 41087 relopabVD 41112 19.41rgVD 41113 ax6e2eqVD 41118 ax6e2ndeqVD 41120 vk15.4jVD 41125 con3ALTVD 41127 |
Copyright terms: Public domain | W3C validator |