![]() |
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 42859 | . 2 ⊢ ( 𝜑 ▶ 𝜒 ) |
4 | e10.3 | . 2 ⊢ (𝜓 → (𝜒 → 𝜃)) | |
5 | 1, 3, 4 | e11 42950 | 1 ⊢ ( 𝜑 ▶ 𝜃 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ( wvd1 42831 |
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 42832 |
This theorem is referenced by: e10an 42957 en3lpVD 43107 3orbi123VD 43112 sbc3orgVD 43113 exbiriVD 43116 3impexpVD 43118 3impexpbicomVD 43119 al2imVD 43124 equncomVD 43130 trsbcVD 43139 sbcssgVD 43145 csbingVD 43146 onfrALTVD 43153 csbsngVD 43155 csbxpgVD 43156 csbresgVD 43157 csbrngVD 43158 csbima12gALTVD 43159 csbunigVD 43160 csbfv12gALTVD 43161 con5VD 43162 hbimpgVD 43166 hbalgVD 43167 hbexgVD 43168 ax6e2eqVD 43169 ax6e2ndeqVD 43171 e2ebindVD 43174 sb5ALTVD 43175 |
Copyright terms: Public domain | W3C validator |