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 59). (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 37846 | . 2 ⊢ ( 𝜑 , 𝜒 ▶ 𝜓 ) |
3 | e12.2 | . 2 ⊢ ( 𝜑 , 𝜒 ▶ 𝜃 ) | |
4 | e12.3 | . 2 ⊢ (𝜓 → (𝜃 → 𝜏)) | |
5 | 2, 3, 4 | e22 37917 | 1 ⊢ ( 𝜑 , 𝜒 ▶ 𝜏 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ( wvd1 37806 ( wvd2 37814 |
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 196 df-an 385 df-vd1 37807 df-vd2 37815 |
This theorem is referenced by: e12an 37973 trsspwALT 38067 sspwtr 38070 pwtrVD 38081 snssiALTVD 38084 elex2VD 38095 elex22VD 38096 eqsbc3rVD 38097 en3lplem1VD 38100 3ornot23VD 38104 orbi1rVD 38105 19.21a3con13vVD 38109 exbirVD 38110 tratrbVD 38119 ssralv2VD 38124 sbcim2gVD 38133 sbcbiVD 38134 relopabVD 38159 19.41rgVD 38160 ax6e2eqVD 38165 ax6e2ndeqVD 38167 vk15.4jVD 38172 con3ALTVD 38174 |
Copyright terms: Public domain | W3C validator |