![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > syl6bir | Structured version Visualization version Unicode version |
Description: A mixed syllogism inference. (Contributed by NM, 18-May-1994.) |
Ref | Expression |
---|---|
syl6bir.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
syl6bir.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
syl6bir |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl6bir.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | biimprd 227 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | syl6bir.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | syl6 34 |
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 189 |
This theorem is referenced by: 19.21t 1988 axext3 2435 tppreqb 4116 issref 5216 sotri2 5232 sotri3 5233 somincom 5237 ordelinel 5524 fnun 5687 fvmpti 5952 ovigg 6422 ndmovg 6457 onint 6627 ordsuc 6646 tfindsg 6692 findsg 6725 zfrep6 6766 extmptsuppeq 6944 tfrlem9 7108 tfr3 7122 omlimcl 7284 oneo 7287 nnneo 7357 pssnn 7795 inficl 7944 dfac2 8566 axdc2lem 8883 axextnd 9021 canthp1lem2 9083 gchinf 9087 inatsk 9208 indpi 9337 ltaddpr2 9465 reclem2pr 9478 supsrlem 9540 axrrecex 9592 zeo 11028 nn0ind-raph 11042 fzm1 11881 fzind2 12030 bcpasc 12513 pr2pwpr 12643 bitsfzo 14421 bezoutlem1 14515 algcvgblem 14548 qredeq 14675 prmreclem2 14873 ramtcl2 14978 ramtcl2OLD 14979 divsfval 15465 joinval 16263 meetval 16277 gsumval3 17553 pgpfac1lem3a 17721 fiinopn 19943 restntr 20210 lly1stc 20523 dgradd2 23234 dgrcolem2 23240 asinneg 23824 ftalem2 24010 ftalem4 24012 ftalem5 24013 ftalem4OLD 24014 ftalem5OLD 24015 bpos1lem 24222 wlkdvspthlem 25349 fargshiftf1 25377 wlknwwlknsur 25452 wlkiswwlksur 25459 clwlkfoclwwlk 25585 hashnbgravdg 25653 cusgraisrusgra 25678 frgrareg 25857 frgraregord013 25858 rngoueqz 26170 h1de2ctlem 27220 pjclem4a 27863 pj3lem1 27871 chrelat2i 28030 sumdmdii 28080 elim2if 28173 bnj1468 29669 bnj517 29708 axextdist 30458 funtransport 30810 bj-19.21t 31444 bj-projval 31602 wl-ax12 31925 areacirc 32049 isdmn3 32319 ax12 32487 lkrlspeqN 32749 hlrelat2 32980 ps-1 33054 dalem54 33303 cdleme42c 34051 dihmeetlem6 34889 frege124d 36365 iotavalb 36792 iccpartnel 38762 gboge7 38874 bgoldbwt 38888 bgoldbtbndlem1 38910 ralnralall 38995 incistruhgr 39181 fusgrfis 39406 uhgrnbgr0nb 39432 cusgrrusgr 39607 |
Copyright terms: Public domain | W3C validator |