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 41965 | 1 ⊢ ( 𝜑 ▶ 𝜃 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ( wvd1 41860 |
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 210 df-vd1 41861 |
This theorem is referenced by: e11an 41980 e01 41982 e10 41985 elex2VD 42129 elex22VD 42130 eqsbc3rVD 42131 tpid3gVD 42133 3ornot23VD 42138 orbi1rVD 42139 3orbi123VD 42141 sbc3orgVD 42142 ordelordALTVD 42158 sbcim2gVD 42166 trsbcVD 42168 undif3VD 42173 sbcssgVD 42174 csbingVD 42175 onfrALTVD 42182 csbeq2gVD 42183 csbsngVD 42184 csbxpgVD 42185 csbresgVD 42186 csbrngVD 42187 csbima12gALTVD 42188 csbunigVD 42189 csbfv12gALTVD 42190 19.41rgVD 42193 2pm13.193VD 42194 hbimpgVD 42195 ax6e2eqVD 42198 2uasbanhVD 42202 notnotrALTVD 42206 |
Copyright terms: Public domain | W3C validator |