![]() |
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 43435 | 1 ⊢ ( 𝜑 ▶ 𝜃 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ( wvd1 43330 |
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 43331 |
This theorem is referenced by: e11an 43450 e01 43452 e10 43455 elex2VD 43599 elex22VD 43600 eqsbc2VD 43601 tpid3gVD 43603 3ornot23VD 43608 orbi1rVD 43609 3orbi123VD 43611 sbc3orgVD 43612 ordelordALTVD 43628 sbcim2gVD 43636 trsbcVD 43638 undif3VD 43643 sbcssgVD 43644 csbingVD 43645 onfrALTVD 43652 csbeq2gVD 43653 csbsngVD 43654 csbxpgVD 43655 csbresgVD 43656 csbrngVD 43657 csbima12gALTVD 43658 csbunigVD 43659 csbfv12gALTVD 43660 19.41rgVD 43663 2pm13.193VD 43664 hbimpgVD 43665 ax6e2eqVD 43668 2uasbanhVD 43672 notnotrALTVD 43676 |
Copyright terms: Public domain | W3C validator |