![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sylan9bbr | Structured version Visualization version 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 711 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | ancoms 459 |
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 377 |
This theorem is referenced by: pm5.75 953 pm5.75OLD 954 sbcom2 2285 sbal1 2300 sbal2 2301 mpteq12f 4493 fmptsng 6109 fconstfvOLD 6152 f1oiso 6267 mpt2eq123 6377 elovmpt2rab 6542 elovmpt2rab1 6543 ovmpt3rabdm 6553 elovmpt3rab1 6554 tfindsg 6714 findsg 6747 dfoprab4f 6878 opiota 6879 fmpt2x 6886 oalimcl 7287 oeeui 7329 nnmword 7360 isinf 7811 elfi 7953 brwdomn0 8110 alephval3 8567 dfac2 8587 fin17 8850 isfin7-2 8852 ltmpi 9355 addclprlem1 9467 distrlem4pr 9477 1idpr 9480 qreccl 11313 0fz1 11848 zmodid2 12157 hashle00 12609 hashfzdm 12645 hashfirdm 12647 dvdseq 14401 sscntz 17029 gexdvds 17284 cnprest 20354 txrest 20695 ptrescn 20703 flimrest 21047 txflf 21070 fclsrest 21088 tsmssubm 21206 mbfi1fseqlem4 22725 axcontlem7 25049 hashecclwwlkn1 25611 usghashecclwwlk 25612 numclwlk1lem2fo 25872 ubthlem1 26561 pjimai 27878 atcv1 28082 chirredi 28096 wl-sbcom2d-lem1 31934 wl-sbalnae 31937 ptrest 31984 poimirlem28 32013 heicant 32020 ftc1anclem1 32062 sbeqi 32448 ralbi12f 32449 iineq12f 32453 nzss 36710 raaan2 38634 uhgreq12g 39202 nbuhgr2vtx1edgb 39470 1wlkcomp 39692 uhgr1wlkspthlem2 39786 clWlkcomp 39805 uhgeq12gALTV 39955 usgpredgv 39984 usgpredgvALT 39985 rngcinv 40256 rngcinvALTV 40268 ringcinv 40307 ringcinvALTV 40331 snlindsntorlem 40536 |
Copyright terms: Public domain | W3C validator |