![]() |
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 43420 | 1 ⊢ ( 𝜑 ▶ 𝜃 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ( wvd1 43315 |
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 43316 |
This theorem is referenced by: e11an 43435 e01 43437 e10 43440 elex2VD 43584 elex22VD 43585 eqsbc2VD 43586 tpid3gVD 43588 3ornot23VD 43593 orbi1rVD 43594 3orbi123VD 43596 sbc3orgVD 43597 ordelordALTVD 43613 sbcim2gVD 43621 trsbcVD 43623 undif3VD 43628 sbcssgVD 43629 csbingVD 43630 onfrALTVD 43637 csbeq2gVD 43638 csbsngVD 43639 csbxpgVD 43640 csbresgVD 43641 csbrngVD 43642 csbima12gALTVD 43643 csbunigVD 43644 csbfv12gALTVD 43645 19.41rgVD 43648 2pm13.193VD 43649 hbimpgVD 43650 ax6e2eqVD 43653 2uasbanhVD 43657 notnotrALTVD 43661 |
Copyright terms: Public domain | W3C validator |