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 77 | . 2 |
4 | 3 | imp 445 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 384 |
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 197 df-an 386 |
This theorem is referenced by: ax8 1996 ax9 2003 rspc2 3320 rspc3v 3325 trintssOLD 4770 copsexg 4956 chfnrn 6328 fvcofneq 6367 ffnfv 6388 f1elima 6520 onint 6995 peano5 7089 f1oweALT 7152 smoel2 7460 pssnn 8178 fiint 8237 dffi2 8329 alephnbtwn 8894 cfcof 9096 zorn2lem7 9324 suplem1pr 9874 addsrpr 9896 mulsrpr 9897 cau3lem 14094 divalglem8 15123 efgi 18132 elfrlmbasn0 20106 locfincmp 21329 tx1stc 21453 fbunfip 21673 filuni 21689 ufileu 21723 rescncf 22700 shmodsi 28248 spanuni 28403 spansneleq 28429 mdi 29154 dmdi 29161 dmdi4 29166 funimass4f 29437 bj-ax89 32667 wl-ax8clv1 33378 wl-ax8clv2 33381 poimirlem32 33441 ffnafv 41251 |
Copyright terms: Public domain | W3C validator |