![]() |
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 44595 | . 2 ⊢ ( 𝜑 ▶ 𝜒 ) |
4 | e10.3 | . 2 ⊢ (𝜓 → (𝜒 → 𝜃)) | |
5 | 1, 3, 4 | e11 44686 | 1 ⊢ ( 𝜑 ▶ 𝜃 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ( wvd1 44567 |
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 44568 |
This theorem is referenced by: e10an 44693 en3lpVD 44843 3orbi123VD 44848 sbc3orgVD 44849 exbiriVD 44852 3impexpVD 44854 3impexpbicomVD 44855 al2imVD 44860 equncomVD 44866 trsbcVD 44875 sbcssgVD 44881 csbingVD 44882 onfrALTVD 44889 csbsngVD 44891 csbxpgVD 44892 csbresgVD 44893 csbrngVD 44894 csbima12gALTVD 44895 csbunigVD 44896 csbfv12gALTVD 44897 con5VD 44898 hbimpgVD 44902 hbalgVD 44903 hbexgVD 44904 ax6e2eqVD 44905 ax6e2ndeqVD 44907 e2ebindVD 44910 sb5ALTVD 44911 |
Copyright terms: Public domain | W3C validator |