Mathbox for Alan Sare |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > e10 | Structured version Visualization version GIF version |
Description: A virtual deduction elimination rule (see mpisyl 21). (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
e10.1 | ⊢ ( 𝜑 ▶ 𝜓 ) |
e10.2 | ⊢ 𝜒 |
e10.3 | ⊢ (𝜓 → (𝜒 → 𝜃)) |
Ref | Expression |
---|---|
e10 | ⊢ ( 𝜑 ▶ 𝜃 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | e10.1 | . 2 ⊢ ( 𝜑 ▶ 𝜓 ) | |
2 | e10.2 | . . 3 ⊢ 𝜒 | |
3 | 2 | vd01 40951 | . 2 ⊢ ( 𝜑 ▶ 𝜒 ) |
4 | e10.3 | . 2 ⊢ (𝜓 → (𝜒 → 𝜃)) | |
5 | 1, 3, 4 | e11 41042 | 1 ⊢ ( 𝜑 ▶ 𝜃 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ( wvd1 40923 |
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 209 df-vd1 40924 |
This theorem is referenced by: e10an 41049 en3lpVD 41199 3orbi123VD 41204 sbc3orgVD 41205 exbiriVD 41208 3impexpVD 41210 3impexpbicomVD 41211 al2imVD 41216 equncomVD 41222 trsbcVD 41231 sbcssgVD 41237 csbingVD 41238 onfrALTVD 41245 csbsngVD 41247 csbxpgVD 41248 csbresgVD 41249 csbrngVD 41250 csbima12gALTVD 41251 csbunigVD 41252 csbfv12gALTVD 41253 con5VD 41254 hbimpgVD 41258 hbalgVD 41259 hbexgVD 41260 ax6e2eqVD 41261 ax6e2ndeqVD 41263 e2ebindVD 41266 sb5ALTVD 41267 |
Copyright terms: Public domain | W3C validator |