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 157 | . 2 |
3 | sylbird.2 | . 2 | |
4 | 2, 3 | syld 45 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: 3imtr3d 201 drex1 1785 eqreu 2913 onsucsssucr 4480 ordsucunielexmid 4502 ovi3 5969 tfrlem9 6278 dom2lem 6729 distrlem4prl 7516 distrlem4pru 7517 recexprlemm 7556 caucvgprlem1 7611 caucvgprprlemexb 7639 aptisr 7711 map2psrprg 7737 renegcl 8150 addid0 8262 remulext2 8489 mulext1 8501 apmul1 8675 nnge1 8871 0mnnnnn0 9137 nn0lt2 9263 zneo 9283 uzind2 9294 fzind 9297 nn0ind-raph 9299 ledivge1le 9653 elfzmlbp 10057 difelfznle 10060 elfzodifsumelfzo 10126 ssfzo12 10149 flqeqceilz 10243 addmodlteq 10323 uzsinds 10367 facdiv 10640 facwordi 10642 bcpasc 10668 addcn2 11237 mulcn2 11239 climrecvg1n 11275 odd2np1 11795 oddge22np1 11803 gcdaddm 11902 algcvgblem 11960 cncongr1 12014 pcdvdsb 12230 pcaddlem 12249 metss2lem 13044 |
Copyright terms: Public domain | W3C validator |