![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > syl9r | Structured version Visualization version Unicode version |
Description: A nested syllogism inference with different antecedents. (Contributed by NM, 14-May-1993.) |
Ref | Expression |
---|---|
syl9r.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
syl9r.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
syl9r |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl9r.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | syl9r.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl9 72 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | com12 31 |
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: sylan9r 670 ax12v2 1952 ax12vOLD 1953 ax12vOLDOLD 1954 19.23tOLD 2012 nfimd 2020 fununi 5659 dfimafn 5928 funimass3 6013 isomin 6246 oneqmin 6651 tz7.48lem 7176 fisupg 7837 fiinfg 8033 trcl 8230 coflim 8709 coftr 8721 axdc3lem2 8899 konigthlem 9011 indpi 9350 nnsub 10670 2ndc1stc 20543 kgencn2 20649 tx1stc 20742 filuni 20978 fclscf 21118 alexsubALTlem2 21141 alexsubALTlem3 21142 alexsubALT 21144 lpni 25990 dfimafnf 28309 dfon2lem6 30505 nodenselem8 30648 finixpnum 31994 heiborlem4 32210 lncvrelatN 33417 imbi13 36947 dfaimafn 38812 |
Copyright terms: Public domain | W3C validator |