![]() |
Mathbox for Alan Sare |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > e11 | Structured version Visualization version GIF version |
Description: A virtual deduction elimination rule. (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
e11.1 | ⊢ ( 𝜑 ▶ 𝜓 ) |
e11.2 | ⊢ ( 𝜑 ▶ 𝜒 ) |
e11.3 | ⊢ (𝜓 → (𝜒 → 𝜃)) |
Ref | Expression |
---|---|
e11 | ⊢ ( 𝜑 ▶ 𝜃 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | e11.1 | . 2 ⊢ ( 𝜑 ▶ 𝜓 ) | |
2 | e11.2 | . 2 ⊢ ( 𝜑 ▶ 𝜒 ) | |
3 | e11.3 | . . 3 ⊢ (𝜓 → (𝜒 → 𝜃)) | |
4 | 3 | a1i 11 | . 2 ⊢ (𝜓 → (𝜓 → (𝜒 → 𝜃))) |
5 | 1, 1, 2, 4 | e111 44255 | 1 ⊢ ( 𝜑 ▶ 𝜃 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ( wvd1 44150 |
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 44151 |
This theorem is referenced by: e11an 44270 e01 44272 e10 44275 elex2VD 44419 elex22VD 44420 eqsbc2VD 44421 tpid3gVD 44423 3ornot23VD 44428 orbi1rVD 44429 3orbi123VD 44431 sbc3orgVD 44432 ordelordALTVD 44448 sbcim2gVD 44456 trsbcVD 44458 undif3VD 44463 sbcssgVD 44464 csbingVD 44465 onfrALTVD 44472 csbeq2gVD 44473 csbsngVD 44474 csbxpgVD 44475 csbresgVD 44476 csbrngVD 44477 csbima12gALTVD 44478 csbunigVD 44479 csbfv12gALTVD 44480 19.41rgVD 44483 2pm13.193VD 44484 hbimpgVD 44485 ax6e2eqVD 44488 2uasbanhVD 44492 notnotrALTVD 44496 |
Copyright terms: Public domain | W3C validator |