Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > sylan9bbr | Unicode version |
Description: Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 4-Mar-1995.) |
Ref | Expression |
---|---|
sylan9bbr.1 | |
sylan9bbr.2 |
Ref | Expression |
---|---|
sylan9bbr |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylan9bbr.1 | . . 3 | |
2 | sylan9bbr.2 | . . 3 | |
3 | 1, 2 | sylan9bb 458 | . 2 |
4 | 3 | ancoms 266 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: pm5.75 951 mpteq12f 4056 opelopabsb 4232 elreimasng 4964 fvelrnb 5528 fmptco 5645 fconstfvm 5697 f1oiso 5788 canth 5790 mpoeq123 5892 dfoprab4f 6153 fmpox 6160 nnmword 6477 elfi 6927 ltmpig 7271 mul0eqap 8558 qreccl 9571 0fz1 9970 zmodid2 10277 divgcdcoprm0 12012 cnptoprest 12786 txrest 12823 cbvrald 13510 |
Copyright terms: Public domain | W3C validator |