![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sylan9bb | Structured version Visualization version 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 472 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | sylan9bb.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | adantl 473 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | bitrd 261 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
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 190 df-an 378 |
This theorem is referenced by: sylan9bbr 715 bi2anan9 890 baibd 923 rbaibd 924 syl3an9b 1363 nanbi12 1423 sbcom2 2294 2sb5rf 2300 2sb6rf 2301 eqeq12 2484 eleq12 2539 sbhypf 3081 ceqsrex2v 3162 sseq12 3441 2ralsng 3999 rexprg 4013 rextpg 4015 breq12 4400 reusv2lem5 4606 opelopabg 4719 brabg 4720 opelopab2 4722 ralxpf 4986 feq23 5723 f00 5778 fconstg 5783 f1oeq23 5821 f1o00 5861 fnelfp 6108 fnelnfp 6110 isofrlem 6249 f1oiso 6260 riota1a 6289 cbvmpt2x 6388 caovord 6499 caovord3 6501 f1oweALT 6796 oaordex 7277 oaass 7280 odi 7298 findcard2s 7830 unfilem1 7853 suppeqfsuppbi 7915 oieu 8072 r1pw 8334 carddomi2 8422 isacn 8493 cdadom2 8635 axdc2 8897 alephval2 9015 fpwwe2cbv 9073 fpwwe2lem2 9075 fpwwecbv 9087 fpwwelem 9088 canthwelem 9093 canthwe 9094 distrlem4pr 9469 axpre-sup 9611 nn0ind-raph 11058 elfz 11816 elfzp12 11899 expeq0 12340 leiso 12663 wrd2ind 12888 trcleq12lem 13132 dfrtrclrec2 13197 shftfib 13212 absdvdsb 14398 dvdsabsb 14399 unbenlem 14931 isprs 16253 isdrs 16257 pltval 16284 lublecllem 16312 istos 16359 isdlat 16517 znfld 19208 tgss2 20080 isopn2 20124 cnpf2 20343 lmbr 20351 isreg2 20470 fclsrest 21117 qustgplem 21213 ustuqtoplem 21332 xmetec 21527 nmogelb 21799 nmogelbOLD 21818 metdstri 21946 metdstriOLD 21961 tchcph 22289 ulmval 23414 iscgrg 24636 eupath2lem1 25784 eigrei 27568 eigorthi 27571 jplem1 28002 superpos 28088 chrelati 28098 br8d 28294 issiga 29007 eulerpartlemgvv 29282 br8 30467 br6 30468 br4 30469 brsegle 30946 topfne 31081 tailfb 31104 filnetlem1 31105 nndivsub 31188 bj-elequ12 31343 isbasisrelowllem1 31828 isbasisrelowllem2 31829 wl-2sb6d 31958 poimirlem26 32030 mblfinlem2 32042 cnambfre 32053 itgaddnclem2 32065 ftc1anclem1 32081 grpokerinj 32247 rngoisoval 32280 smprngopr 32349 ax12eq 32576 ax12el 32577 2llnjN 33203 2lplnj 33256 elpadd0 33445 lauteq 33731 lpolconN 35126 rexrabdioph 35708 eliunov2 36342 nzss 36736 iotasbc2 36841 xnn0xadd0 39238 istrlson 39902 ispthson 39934 isspthson 39935 eupth2lem1 40130 uhg0e 40196 cbvmpt2x2 40625 |
Copyright terms: Public domain | W3C validator |