![]() |
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 39173 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 39118 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) |
3 | e2.2 | . . 3 ⊢ (𝜒 → 𝜃) | |
4 | 2, 3 | syl6 35 | . 2 ⊢ (𝜑 → (𝜓 → 𝜃)) |
5 | 4 | dfvd2ir 39119 | 1 ⊢ ( 𝜑 , 𝜓 ▶ 𝜃 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ( wvd2 39110 |
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 197 df-an 385 df-vd2 39111 |
This theorem is referenced by: e2bi 39174 e2bir 39175 sspwtr 39365 pwtrVD 39373 pwtrrVD 39374 suctrALT2VD 39385 tpid3gVD 39391 en3lplem1VD 39392 3ornot23VD 39396 orbi1rVD 39397 19.21a3con13vVD 39401 tratrbVD 39411 syl5impVD 39413 ssralv2VD 39416 truniALTVD 39428 trintALTVD 39430 onfrALTlem3VD 39437 onfrALTlem2VD 39439 onfrALTlem1VD 39440 relopabVD 39451 19.41rgVD 39452 hbimpgVD 39454 ax6e2eqVD 39457 ax6e2ndeqVD 39459 sb5ALTVD 39463 vk15.4jVD 39464 con3ALTVD 39466 |
Copyright terms: Public domain | W3C validator |