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 156 | . 2 |
3 | sylbird.2 | . 2 | |
4 | 2, 3 | syld 44 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 103 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: 3imtr3d 200 drex1 1719 eqreu 2784 onsucsssucr 4253 ordsucunielexmid 4274 ovi3 5657 tfrlem9 5958 rdgon 5996 dom2lem 6275 distrlem4prl 6774 distrlem4pru 6775 recexprlemm 6814 caucvgprlem1 6869 caucvgprprlemexb 6897 aptisr 6955 renegcl 7369 addid0 7477 remulext2 7700 mulext1 7712 apmul1 7876 nnge1 8062 0mnnnnn0 8320 nn0lt2 8429 zneo 8448 uzind2 8459 fzind 8462 nn0ind-raph 8464 ledivge1le 8803 elfzmlbp 9143 difelfznle 9146 elfzodifsumelfzo 9210 ssfzo12 9233 flqeqceilz 9320 addmodlteq 9400 uzsinds 9428 facdiv 9665 facwordi 9667 bcpasc 9693 addcn2 10149 mulcn2 10151 climrecvg1n 10185 odd2np1 10272 oddge22np1 10281 gcdaddm 10375 algcvgblem 10431 cncongr1 10485 |
Copyright terms: Public domain | W3C validator |