![]() |
Mathbox for Alan Sare |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > e1a | Structured version Visualization version GIF version |
Description: A Virtual deduction elimination rule. syl 17 is e1a 44340 without virtual deductions. (Contributed by Alan Sare, 11-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
e1a.1 | ⊢ ( 𝜑 ▶ 𝜓 ) |
e1a.2 | ⊢ (𝜓 → 𝜒) |
Ref | Expression |
---|---|
e1a | ⊢ ( 𝜑 ▶ 𝜒 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | e1a.1 | . . . 4 ⊢ ( 𝜑 ▶ 𝜓 ) | |
2 | 1 | in1 44284 | . . 3 ⊢ (𝜑 → 𝜓) |
3 | e1a.2 | . . 3 ⊢ (𝜓 → 𝜒) | |
4 | 2, 3 | syl 17 | . 2 ⊢ (𝜑 → 𝜒) |
5 | 4 | dfvd1ir 44286 | 1 ⊢ ( 𝜑 ▶ 𝜒 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ( wvd1 44282 |
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-vd1 44283 |
This theorem is referenced by: e1bi 44342 e1bir 44343 snelpwrVD 44544 unipwrVD 44545 sstrALT2VD 44547 elex2VD 44551 elex22VD 44552 eqsbc2VD 44553 zfregs2VD 44554 tpid3gVD 44555 en3lplem1VD 44556 en3lpVD 44558 3ornot23VD 44560 3orbi123VD 44563 sbc3orgVD 44564 exbirVD 44566 3impexpVD 44569 3impexpbicomVD 44570 tratrbVD 44574 al2imVD 44575 syl5impVD 44576 ssralv2VD 44579 ordelordALTVD 44580 sbcim2gVD 44588 trsbcVD 44590 truniALTVD 44591 trintALTVD 44593 undif3VD 44595 sbcssgVD 44596 csbingVD 44597 onfrALTlem3VD 44600 simplbi2comtVD 44601 onfrALTlem2VD 44602 onfrALTVD 44604 csbeq2gVD 44605 csbsngVD 44606 csbxpgVD 44607 csbresgVD 44608 csbrngVD 44609 csbima12gALTVD 44610 csbunigVD 44611 csbfv12gALTVD 44612 con5VD 44613 relopabVD 44614 19.41rgVD 44615 2pm13.193VD 44616 hbimpgVD 44617 hbalgVD 44618 hbexgVD 44619 ax6e2eqVD 44620 ax6e2ndVD 44621 ax6e2ndeqVD 44622 2sb5ndVD 44623 2uasbanhVD 44624 e2ebindVD 44625 sb5ALTVD 44626 vk15.4jVD 44627 notnotrALTVD 44628 con3ALTVD 44629 |
Copyright terms: Public domain | W3C validator |