![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > syl23anc | Structured version Unicode version |
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
Ref | Expression |
---|---|
sylXanc.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
sylXanc.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
sylXanc.3 |
![]() ![]() ![]() ![]() ![]() ![]() |
sylXanc.4 |
![]() ![]() ![]() ![]() ![]() ![]() |
sylXanc.5 |
![]() ![]() ![]() ![]() ![]() ![]() |
syl23anc.6 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
syl23anc |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylXanc.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | sylXanc.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | jca 532 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | sylXanc.3 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
5 | sylXanc.4 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
6 | sylXanc.5 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
7 | syl23anc.6 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | 3, 4, 5, 6, 7 | syl13anc 1221 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
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 185 df-an 371 df-3an 967 |
This theorem is referenced by: suppofss1d 6829 suppofss2d 6830 cnfcomlem 8036 cnfcomlemOLD 8044 ackbij1lem16 8508 div2subd 10261 symg2bas 16014 evl1expd 17897 psgndiflemA 18149 oftpos 18453 restopn2 18906 tsmsxp 19854 blcld 20205 metustexhalfOLD 20263 metustexhalf 20264 cnllycmp 20653 dvlipcn 21592 tanregt0 22121 ostthlem1 23002 ax5seglem6 23325 axcontlem4 23358 axcontlem7 23361 pnfneige0 26519 qqhval2 26549 esumcocn 26667 heiborlem8 28858 mpaaeu 29648 wwlkextwrd 30501 bnj1125 32286 2atjm 33398 1cvrat 33429 lvolnlelln 33537 lvolnlelpln 33538 4atlem3 33549 lplncvrlvol 33569 dalem39 33664 cdleme4a 34192 cdleme15 34231 cdleme16c 34233 cdleme19b 34257 cdleme19e 34260 cdleme20d 34265 cdleme20g 34268 cdleme20j 34271 cdleme20k 34272 cdleme20l2 34274 cdleme20l 34275 cdleme20m 34276 cdleme22e 34297 cdleme22eALTN 34298 cdleme22f 34299 cdleme27cl 34319 cdlemefr27cl 34356 |
Copyright terms: Public domain | W3C validator |