![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > sylan9 | 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 71 | . 2 |
4 | 3 | imp 429 | 1 |
Colors of variables: wff setvar class |
Syntax hints: -> wi 4 /\ wa 369 |
This theorem is referenced by: rspc2 3218 rspc3v 3222 trintss 4561 copsexg 4737 copsexgOLD 4738 chfnrn 5998 fvcofneq 6039 ffnfv 6057 f1elima 6171 onint 6630 peano5 6723 f1oweALT 6784 smoel2 7053 pssnn 7758 fiint 7817 dffi2 7903 alephnbtwn 8473 cfcof 8675 zorn2lem7 8903 suplem1pr 9451 addsrpr 9473 mulsrpr 9474 cau3lem 13187 divalglem8 14058 efgi 16737 elfrlmbasn0 18796 locfincmp 20027 tx1stc 20151 fbunfip 20370 filuni 20386 ufileu 20420 rescncf 21401 shmodsi 26307 spanuni 26462 spansneleq 26488 mdi 27214 dmdi 27221 dmdi4 27226 funimass4f 27474 ffnafv 32256 bj-ax89 34238 |
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 |
Copyright terms: Public domain | W3C validator |