Higher-Order Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > HOLE Home > Th. List > syl | Unicode version |
Description: Syllogism inference. |
Ref | Expression |
---|---|
ax-syl.1 | |
ax-syl.2 |
Ref | Expression |
---|---|
syl |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-syl.1 | . 2 | |
2 | ax-syl.2 | . 2 | |
3 | 1, 2 | ax-syl 15 | 1 |
Colors of variables: type var term |
Syntax hints: wffMMJ2 11 |
This theorem was proved from axioms: ax-syl 15 |
This theorem is referenced by: syl2anc 19 a1i 28 simpld 35 simprd 36 adantr 50 pm2.21 143 con3d 152 ecase 153 exlimdv2 156 cla4ev 159 19.8a 160 eta 166 exlimd 171 eximdv 173 exnal1 175 ac 184 exmid 186 notnot 187 ax3 192 ax7 196 ax9 199 ax11 201 axrep 207 axpow 208 axun 209 |
Copyright terms: Public domain | W3C validator |