![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sylan9 | Structured version Visualization version Unicode version |
Description: Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 14-May-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
Ref | Expression |
---|---|
sylan9.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
sylan9.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
sylan9 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylan9.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | sylan9.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl9 73 |
. 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: rspc2 3158 rspc3v 3162 trintss 4513 copsexg 4687 chfnrn 5993 fvcofneq 6030 ffnfv 6049 f1elima 6164 onint 6622 peano5 6716 f1oweALT 6777 smoel2 7082 pssnn 7790 fiint 7848 dffi2 7937 alephnbtwn 8502 cfcof 8704 zorn2lem7 8932 suplem1pr 9477 addsrpr 9499 mulsrpr 9500 cau3lem 13417 divalglem8 14380 efgi 17369 elfrlmbasn0 19325 locfincmp 20541 tx1stc 20665 fbunfip 20884 filuni 20900 ufileu 20934 rescncf 21929 shmodsi 27042 spanuni 27197 spansneleq 27223 mdi 27948 dmdi 27955 dmdi4 27960 funimass4f 28234 bj-ax89 31276 poimirlem32 31972 ffnafv 38673 |
Copyright terms: Public domain | W3C validator |