![]() |
Mathbox for Alan Sare |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > e1a | Structured version Visualization version GIF version |
Description: A Virtual deduction elimination rule. syl 17 is e1a 44625 without virtual deductions. (Contributed by Alan Sare, 11-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
e1a.1 | ⊢ ( 𝜑 ▶ 𝜓 ) |
e1a.2 | ⊢ (𝜓 → 𝜒) |
Ref | Expression |
---|---|
e1a | ⊢ ( 𝜑 ▶ 𝜒 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | e1a.1 | . . . 4 ⊢ ( 𝜑 ▶ 𝜓 ) | |
2 | 1 | in1 44569 | . . 3 ⊢ (𝜑 → 𝜓) |
3 | e1a.2 | . . 3 ⊢ (𝜓 → 𝜒) | |
4 | 2, 3 | syl 17 | . 2 ⊢ (𝜑 → 𝜒) |
5 | 4 | dfvd1ir 44571 | 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: e1bi 44627 e1bir 44628 snelpwrVD 44829 unipwrVD 44830 sstrALT2VD 44832 elex2VD 44836 elex22VD 44837 eqsbc2VD 44838 zfregs2VD 44839 tpid3gVD 44840 en3lplem1VD 44841 en3lpVD 44843 3ornot23VD 44845 3orbi123VD 44848 sbc3orgVD 44849 exbirVD 44851 3impexpVD 44854 3impexpbicomVD 44855 tratrbVD 44859 al2imVD 44860 syl5impVD 44861 ssralv2VD 44864 ordelordALTVD 44865 sbcim2gVD 44873 trsbcVD 44875 truniALTVD 44876 trintALTVD 44878 undif3VD 44880 sbcssgVD 44881 csbingVD 44882 onfrALTlem3VD 44885 simplbi2comtVD 44886 onfrALTlem2VD 44887 onfrALTVD 44889 csbeq2gVD 44890 csbsngVD 44891 csbxpgVD 44892 csbresgVD 44893 csbrngVD 44894 csbima12gALTVD 44895 csbunigVD 44896 csbfv12gALTVD 44897 con5VD 44898 relopabVD 44899 19.41rgVD 44900 2pm13.193VD 44901 hbimpgVD 44902 hbalgVD 44903 hbexgVD 44904 ax6e2eqVD 44905 ax6e2ndVD 44906 ax6e2ndeqVD 44907 2sb5ndVD 44908 2uasbanhVD 44909 e2ebindVD 44910 sb5ALTVD 44911 vk15.4jVD 44912 notnotrALTVD 44913 con3ALTVD 44914 |
Copyright terms: Public domain | W3C validator |