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 37843 | . 2 ⊢ ( 𝜑 ▶ 𝜒 ) |
4 | e10.3 | . 2 ⊢ (𝜓 → (𝜒 → 𝜃)) | |
5 | 1, 3, 4 | e11 37934 | 1 ⊢ ( 𝜑 ▶ 𝜃 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ( wvd1 37806 |
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 196 df-vd1 37807 |
This theorem is referenced by: e10an 37941 en3lpVD 38102 3orbi123VD 38107 sbc3orgVD 38108 exbiriVD 38111 3impexpVD 38113 3impexpbicomVD 38114 al2imVD 38120 equncomVD 38126 trsbcVD 38135 sbcssgVD 38141 csbingVD 38142 onfrALTVD 38149 csbsngVD 38151 csbxpgVD 38152 csbresgVD 38153 csbrngVD 38154 csbima12gALTVD 38155 csbunigVD 38156 csbfv12gALTVD 38157 con5VD 38158 hbimpgVD 38162 hbalgVD 38163 hbexgVD 38164 ax6e2eqVD 38165 ax6e2ndeqVD 38167 e2ebindVD 38170 sb5ALTVD 38171 |
Copyright terms: Public domain | W3C validator |