![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > biimtrrdi | GIF version |
Description: A mixed syllogism inference. (Contributed by NM, 18-May-1994.) |
Ref | Expression |
---|---|
biimtrrdi.1 | ⊢ (𝜑 → (𝜒 ↔ 𝜓)) |
biimtrrdi.2 | ⊢ (𝜒 → 𝜃) |
Ref | Expression |
---|---|
biimtrrdi | ⊢ (𝜑 → (𝜓 → 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biimtrrdi.1 | . . 3 ⊢ (𝜑 → (𝜒 ↔ 𝜓)) | |
2 | 1 | biimprd 158 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) |
3 | biimtrrdi.2 | . 2 ⊢ (𝜒 → 𝜃) | |
4 | 2, 3 | syl6 33 | 1 ⊢ (𝜑 → (𝜓 → 𝜃)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 105 |
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: exdistrfor 1811 cbvexdh 1938 repizf2 4183 issref 5032 fnun 5344 ovigg 6021 tfrlem9 6348 tfri3 6396 ordge1n0im 6465 nntri3or 6522 updjud 7115 axprecex 7914 peano5nnnn 7926 peano5nni 8957 zeo 9393 nn0ind-raph 9405 fzm1 10136 fzind2 10275 fzfig 10467 bcpasc 10787 climrecvg1n 11397 oddnn02np1 11926 oddge22np1 11927 evennn02n 11928 evennn2n 11929 gcdaddm 12026 coprmdvds1 12134 qredeq 12139 fiinopn 13989 zabsle1 14886 bj-intabssel 15027 triap 15265 |
Copyright terms: Public domain | W3C validator |