![]() |
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 44057 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 44001 | . . 3 ⊢ (𝜑 → 𝜓) |
3 | e1a.2 | . . 3 ⊢ (𝜓 → 𝜒) | |
4 | 2, 3 | syl 17 | . 2 ⊢ (𝜑 → 𝜒) |
5 | 4 | dfvd1ir 44003 | 1 ⊢ ( 𝜑 ▶ 𝜒 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ( wvd1 43999 |
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 44000 |
This theorem is referenced by: e1bi 44059 e1bir 44060 snelpwrVD 44261 unipwrVD 44262 sstrALT2VD 44264 elex2VD 44268 elex22VD 44269 eqsbc2VD 44270 zfregs2VD 44271 tpid3gVD 44272 en3lplem1VD 44273 en3lpVD 44275 3ornot23VD 44277 3orbi123VD 44280 sbc3orgVD 44281 exbirVD 44283 3impexpVD 44286 3impexpbicomVD 44287 tratrbVD 44291 al2imVD 44292 syl5impVD 44293 ssralv2VD 44296 ordelordALTVD 44297 sbcim2gVD 44305 trsbcVD 44307 truniALTVD 44308 trintALTVD 44310 undif3VD 44312 sbcssgVD 44313 csbingVD 44314 onfrALTlem3VD 44317 simplbi2comtVD 44318 onfrALTlem2VD 44319 onfrALTVD 44321 csbeq2gVD 44322 csbsngVD 44323 csbxpgVD 44324 csbresgVD 44325 csbrngVD 44326 csbima12gALTVD 44327 csbunigVD 44328 csbfv12gALTVD 44329 con5VD 44330 relopabVD 44331 19.41rgVD 44332 2pm13.193VD 44333 hbimpgVD 44334 hbalgVD 44335 hbexgVD 44336 ax6e2eqVD 44337 ax6e2ndVD 44338 ax6e2ndeqVD 44339 2sb5ndVD 44340 2uasbanhVD 44341 e2ebindVD 44342 sb5ALTVD 44343 vk15.4jVD 44344 notnotrALTVD 44345 con3ALTVD 44346 |
Copyright terms: Public domain | W3C validator |