![]() |
Mathbox for Alan Sare |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > e2 | Structured version Visualization version GIF version |
Description: A virtual deduction elimination rule. syl6 35 is e2 43377 without virtual deductions. (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
e2.1 | ⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) |
e2.2 | ⊢ (𝜒 → 𝜃) |
Ref | Expression |
---|---|
e2 | ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | e2.1 | . . . 4 ⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) | |
2 | 1 | dfvd2i 43331 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) |
3 | e2.2 | . . 3 ⊢ (𝜒 → 𝜃) | |
4 | 2, 3 | syl6 35 | . 2 ⊢ (𝜑 → (𝜓 → 𝜃)) |
5 | 4 | dfvd2ir 43332 | 1 ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ( 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-vd2 43324 |
This theorem is referenced by: e2bi 43378 e2bir 43379 sspwtr 43567 pwtrVD 43570 pwtrrVD 43571 suctrALT2VD 43582 tpid3gVD 43588 en3lplem1VD 43589 3ornot23VD 43593 orbi1rVD 43594 19.21a3con13vVD 43598 tratrbVD 43607 syl5impVD 43609 ssralv2VD 43612 truniALTVD 43624 trintALTVD 43626 onfrALTlem3VD 43633 onfrALTlem2VD 43635 onfrALTlem1VD 43636 relopabVD 43647 19.41rgVD 43648 hbimpgVD 43650 ax6e2eqVD 43653 ax6e2ndeqVD 43655 sb5ALTVD 43659 vk15.4jVD 43660 con3ALTVD 43662 |
Copyright terms: Public domain | W3C validator |