![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > sylbird | Unicode version |
Description: A syllogism deduction. (Contributed by NM, 3-Aug-1994.) |
Ref | Expression |
---|---|
sylbird.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
sylbird.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
sylbird |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylbird.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | biimprd 158 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | sylbird.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | syld 45 |
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: 3imtr3d 202 drex1 1798 eqreu 2929 onsucsssucr 4504 ordsucunielexmid 4526 ovi3 6004 tfrlem9 6313 dom2lem 6765 distrlem4prl 7561 distrlem4pru 7562 recexprlemm 7601 caucvgprlem1 7656 caucvgprprlemexb 7684 aptisr 7756 map2psrprg 7782 renegcl 8195 addid0 8307 remulext2 8534 mulext1 8546 apmul1 8721 nnge1 8918 0mnnnnn0 9184 nn0lt2 9310 zneo 9330 uzind2 9341 fzind 9344 nn0ind-raph 9346 ledivge1le 9700 elfzmlbp 10105 difelfznle 10108 elfzodifsumelfzo 10174 ssfzo12 10197 flqeqceilz 10291 addmodlteq 10371 uzsinds 10415 qsqeqor 10603 facdiv 10689 facwordi 10691 bcpasc 10717 addcn2 11289 mulcn2 11291 climrecvg1n 11327 odd2np1 11848 oddge22np1 11856 gcdaddm 11955 algcvgblem 12019 cncongr1 12073 pcdvdsb 12289 pcaddlem 12308 infpnlem1 12327 prmunb 12330 metss2lem 13630 2sqlem6 14089 |
Copyright terms: Public domain | W3C validator |