Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > sylan9bb | Unicode version |
Description: Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 4-Mar-1995.) |
Ref | Expression |
---|---|
sylan9bb.1 | |
sylan9bb.2 |
Ref | Expression |
---|---|
sylan9bb |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylan9bb.1 | . . 3 | |
2 | 1 | adantr 274 | . 2 |
3 | sylan9bb.2 | . . 3 | |
4 | 3 | adantl 275 | . 2 |
5 | 2, 4 | bitrd 187 | 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: sylan9bbr 458 bi2anan9 595 baibd 908 rbaibd 909 syl3an9b 1288 sbcomxyyz 1943 eqeq12 2150 eleq12 2202 sbhypf 2730 ceqsrex2v 2812 sseq12 3117 rexprg 3570 rextpg 3572 breq12 3929 opelopabg 4185 brabg 4186 opelopab2 4187 ralxpf 4680 rexxpf 4681 feq23 5253 f00 5309 fconstg 5314 f1oeq23 5354 f1o00 5395 f1oiso 5720 riota1a 5742 cbvmpox 5842 caovord 5935 caovord3 5937 rbropapd 6132 genpelvl 7313 genpelvu 7314 nn0ind-raph 9161 xnn0xadd0 9643 elfz 9789 elfzp12 9872 shftfibg 10585 shftfib 10588 absdvdsb 11500 dvdsabsb 11501 dvdsabseq 11534 tgss2 12237 lmbr 12371 xmetec 12595 |
Copyright terms: Public domain | W3C validator |