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 1780 cbvexdh 1906 repizf2 4123 issref 4968 fnun 5276 ovigg 5941 tfrlem9 6266 tfri3 6314 ordge1n0im 6383 nntri3or 6440 updjud 7026 axprecex 7800 peano5nnnn 7812 peano5nni 8836 zeo 9269 nn0ind-raph 9281 fzm1 10002 fzind2 10138 fzfig 10329 bcpasc 10640 climrecvg1n 11245 oddnn02np1 11771 oddge22np1 11772 evennn02n 11773 evennn2n 11774 gcdaddm 11868 coprmdvds1 11968 qredeq 11973 fiinopn 12413 bj-intabssel 13374 triap 13611 |
Copyright terms: Public domain | W3C validator |