![]() |
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 276 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | sylan9bb.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | adantl 277 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | bitrd 188 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: sylan9bbr 463 bi2anan9 606 baibd 923 rbaibd 924 syl3an9b 1310 sbcomxyyz 1972 eqeq12 2190 eleq12 2242 sbhypf 2786 ceqsrex2v 2869 sseq12 3180 rexprg 3644 rextpg 3646 breq12 4008 opelopabg 4268 brabg 4269 opelopab2 4270 ralxpf 4773 rexxpf 4774 feq23 5351 f00 5407 fconstg 5412 f1oeq23 5452 f1o00 5496 f1oiso 5826 riota1a 5849 cbvmpox 5952 caovord 6045 caovord3 6047 rbropapd 6242 genpelvl 7510 genpelvu 7511 nn0ind-raph 9368 elpq 9646 xnn0xadd0 9865 elfz 10012 elfzp12 10096 shftfibg 10824 shftfib 10827 absdvdsb 11811 dvdsabsb 11812 dvdsabseq 11847 tgss2 13472 lmbr 13606 xmetec 13830 |
Copyright terms: Public domain | W3C validator |