![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > syl7 | Structured version Visualization version Unicode version |
Description: A syllogism rule of inference. The first premise is used to replace the third antecedent of the second premise. (Contributed by NM, 12-Jan-1993.) (Proof shortened by Wolf Lammen, 3-Aug-2012.) |
Ref | Expression |
---|---|
syl7.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
syl7.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
syl7 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl7.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | a1i 11 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | syl7.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | syl5d 69 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 |
This theorem is referenced by: syl7bi 234 syl3an3 1303 hbae 2149 tz7.7 5449 fvmptt 5965 f1oweALT 6777 wfrlem12 7047 nneneq 7755 pr2nelem 8435 cfcoflem 8702 nnunb 10865 ndvdssub 14388 lsmcv 18364 gsummoncoe1 18898 uvcendim 19405 2ndcsep 20474 atcvat4i 28050 mdsymlem5 28060 sumdmdii 28068 dfon2lem6 30434 frrlem11 30526 colineardim1 30828 bj-hbaeb2 31420 wl-ax12 31913 hbae-o 32473 ax12 32475 cvrat4 33008 llncvrlpln2 33122 lplncvrlvol2 33180 dihmeetlem3N 34873 eel2122old 37103 |
Copyright terms: Public domain | W3C validator |