Mathbox for Alan Sare |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > e1a | Structured version Visualization version Unicode version |
Description: A Virtual deduction elimination rule. syl 17 is e1a 38852 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 38787 | . . 3 |
3 | e1a.2 | . . 3 | |
4 | 2, 3 | syl 17 | . 2 |
5 | 4 | dfvd1ir 38789 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wvd1 38785 |
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 197 df-vd1 38786 |
This theorem is referenced by: e1bi 38854 e1bir 38855 snelpwrVD 39066 unipwrVD 39067 sstrALT2VD 39069 elex2VD 39073 elex22VD 39074 eqsbc3rVD 39075 zfregs2VD 39076 tpid3gVD 39077 en3lplem1VD 39078 en3lpVD 39080 3ornot23VD 39082 3orbi123VD 39085 sbc3orgVD 39086 exbirVD 39088 3impexpVD 39091 3impexpbicomVD 39092 sbcoreleleqVD 39095 tratrbVD 39097 al2imVD 39098 syl5impVD 39099 ssralv2VD 39102 ordelordALTVD 39103 sbcim2gVD 39111 trsbcVD 39113 truniALTVD 39114 trintALTVD 39116 undif3VD 39118 sbcssgVD 39119 csbingVD 39120 onfrALTlem3VD 39123 simplbi2comtVD 39124 onfrALTlem2VD 39125 onfrALTVD 39127 csbeq2gVD 39128 csbsngVD 39129 csbxpgVD 39130 csbresgVD 39131 csbrngVD 39132 csbima12gALTVD 39133 csbunigVD 39134 csbfv12gALTVD 39135 con5VD 39136 relopabVD 39137 19.41rgVD 39138 2pm13.193VD 39139 hbimpgVD 39140 hbalgVD 39141 hbexgVD 39142 ax6e2eqVD 39143 ax6e2ndVD 39144 ax6e2ndeqVD 39145 2sb5ndVD 39146 2uasbanhVD 39147 e2ebindVD 39148 sb5ALTVD 39149 vk15.4jVD 39150 notnotrALTVD 39151 con3ALTVD 39152 |
Copyright terms: Public domain | W3C validator |