| 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 44617 | . 2 ⊢ ( 𝜑 ▶ 𝜒 ) |
| 4 | e10.3 | . 2 ⊢ (𝜓 → (𝜒 → 𝜃)) | |
| 5 | 1, 3, 4 | e11 44708 | 1 ⊢ ( 𝜑 ▶ 𝜃 ) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ( wvd1 44589 |
| 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 207 df-vd1 44590 |
| This theorem is referenced by: e10an 44715 en3lpVD 44865 3orbi123VD 44870 sbc3orgVD 44871 exbiriVD 44874 3impexpVD 44876 3impexpbicomVD 44877 al2imVD 44882 equncomVD 44888 trsbcVD 44897 sbcssgVD 44903 csbingVD 44904 onfrALTVD 44911 csbsngVD 44913 csbxpgVD 44914 csbresgVD 44915 csbrngVD 44916 csbima12gALTVD 44917 csbunigVD 44918 csbfv12gALTVD 44919 con5VD 44920 hbimpgVD 44924 hbalgVD 44925 hbexgVD 44926 ax6e2eqVD 44927 ax6e2ndeqVD 44929 e2ebindVD 44932 sb5ALTVD 44933 |
| Copyright terms: Public domain | W3C validator |