![]() |
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 43321 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 43265 | . . 3 ⊢ (𝜑 → 𝜓) |
3 | e1a.2 | . . 3 ⊢ (𝜓 → 𝜒) | |
4 | 2, 3 | syl 17 | . 2 ⊢ (𝜑 → 𝜒) |
5 | 4 | dfvd1ir 43267 | 1 ⊢ ( 𝜑 ▶ 𝜒 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ( wvd1 43263 |
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 43264 |
This theorem is referenced by: e1bi 43323 e1bir 43324 snelpwrVD 43525 unipwrVD 43526 sstrALT2VD 43528 elex2VD 43532 elex22VD 43533 eqsbc2VD 43534 zfregs2VD 43535 tpid3gVD 43536 en3lplem1VD 43537 en3lpVD 43539 3ornot23VD 43541 3orbi123VD 43544 sbc3orgVD 43545 exbirVD 43547 3impexpVD 43550 3impexpbicomVD 43551 tratrbVD 43555 al2imVD 43556 syl5impVD 43557 ssralv2VD 43560 ordelordALTVD 43561 sbcim2gVD 43569 trsbcVD 43571 truniALTVD 43572 trintALTVD 43574 undif3VD 43576 sbcssgVD 43577 csbingVD 43578 onfrALTlem3VD 43581 simplbi2comtVD 43582 onfrALTlem2VD 43583 onfrALTVD 43585 csbeq2gVD 43586 csbsngVD 43587 csbxpgVD 43588 csbresgVD 43589 csbrngVD 43590 csbima12gALTVD 43591 csbunigVD 43592 csbfv12gALTVD 43593 con5VD 43594 relopabVD 43595 19.41rgVD 43596 2pm13.193VD 43597 hbimpgVD 43598 hbalgVD 43599 hbexgVD 43600 ax6e2eqVD 43601 ax6e2ndVD 43602 ax6e2ndeqVD 43603 2sb5ndVD 43604 2uasbanhVD 43605 e2ebindVD 43606 sb5ALTVD 43607 vk15.4jVD 43608 notnotrALTVD 43609 con3ALTVD 43610 |
Copyright terms: Public domain | W3C validator |