![]() |
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 43382 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 43336 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) |
3 | e2.2 | . . 3 ⊢ (𝜒 → 𝜃) | |
4 | 2, 3 | syl6 35 | . 2 ⊢ (𝜑 → (𝜓 → 𝜃)) |
5 | 4 | dfvd2ir 43337 | 1 ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ( wvd2 43328 |
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 43329 |
This theorem is referenced by: e2bi 43383 e2bir 43384 sspwtr 43572 pwtrVD 43575 pwtrrVD 43576 suctrALT2VD 43587 tpid3gVD 43593 en3lplem1VD 43594 3ornot23VD 43598 orbi1rVD 43599 19.21a3con13vVD 43603 tratrbVD 43612 syl5impVD 43614 ssralv2VD 43617 truniALTVD 43629 trintALTVD 43631 onfrALTlem3VD 43638 onfrALTlem2VD 43640 onfrALTlem1VD 43641 relopabVD 43652 19.41rgVD 43653 hbimpgVD 43655 ax6e2eqVD 43658 ax6e2ndeqVD 43660 sb5ALTVD 43664 vk15.4jVD 43665 con3ALTVD 43667 |
Copyright terms: Public domain | W3C validator |