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 40885 | 1 ⊢ ( 𝜑 ▶ 𝜃 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ( wvd1 40780 |
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 208 df-vd1 40781 |
This theorem is referenced by: e11an 40900 e01 40902 e10 40905 elex2VD 41049 elex22VD 41050 eqsbc3rVD 41051 tpid3gVD 41053 3ornot23VD 41058 orbi1rVD 41059 3orbi123VD 41061 sbc3orgVD 41062 ordelordALTVD 41078 sbcim2gVD 41086 trsbcVD 41088 undif3VD 41093 sbcssgVD 41094 csbingVD 41095 onfrALTVD 41102 csbeq2gVD 41103 csbsngVD 41104 csbxpgVD 41105 csbresgVD 41106 csbrngVD 41107 csbima12gALTVD 41108 csbunigVD 41109 csbfv12gALTVD 41110 19.41rgVD 41113 2pm13.193VD 41114 hbimpgVD 41115 ax6e2eqVD 41118 2uasbanhVD 41122 notnotrALTVD 41126 |
Copyright terms: Public domain | W3C validator |