![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sylan9r | Structured version Visualization version Unicode version |
Description: Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 14-May-1993.) |
Ref | Expression |
---|---|
sylan9r.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
sylan9r.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
sylan9r |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylan9r.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | sylan9r.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl9r 74 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | imp 431 |
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 189 df-an 373 |
This theorem is referenced by: spimt 2097 limsssuc 6677 tfindsg 6687 findsg 6720 f1oweALT 6777 oaordi 7247 pssnn 7790 inf3lem2 8134 cardlim 8406 ac10ct 8465 cardaleph 8520 cfub 8679 cfcoflem 8702 hsmexlem2 8857 zorn2lem7 8932 pwcfsdom 9008 grur1a 9244 genpcd 9431 supadd 10575 supmul 10579 zeo 11021 uzwo 11222 xrub 11597 iccsupr 11727 reuccats1lem 12836 climuni 13616 efgi2 17375 opnnei 20136 tgcn 20268 locfincf 20546 uffix 20936 alexsubALTlem2 21063 alexsubALT 21066 metrest 21539 causs 22268 subgoablo 26039 ocin 26949 spanuni 27197 superpos 28007 bnj518 29697 3orel13 30349 trpredmintr 30472 frmin 30480 nndivsub 31117 bj-spimtv 31319 cover2 32040 metf1o 32084 intabssd 36216 stoweidlem62 37923 stoweidlem62OLD 37924 reuccatpfxs1lem 38974 |
Copyright terms: Public domain | W3C validator |