Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > syl6bir | 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 157 | . 2 |
3 | syl6bir.2 | . 2 | |
4 | 2, 3 | syl6 33 | 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: exdistrfor 1772 cbvexdh 1898 repizf2 4086 issref 4921 fnun 5229 ovigg 5891 tfrlem9 6216 tfri3 6264 ordge1n0im 6333 nntri3or 6389 updjud 6967 axprecex 7688 peano5nnnn 7700 peano5nni 8723 zeo 9156 nn0ind-raph 9168 fzm1 9880 fzind2 10016 fzfig 10203 bcpasc 10512 climrecvg1n 11117 oddnn02np1 11577 oddge22np1 11578 evennn02n 11579 evennn2n 11580 gcdaddm 11672 coprmdvds1 11772 qredeq 11777 fiinopn 12171 bj-intabssel 12996 triap 13224 |
Copyright terms: Public domain | W3C validator |