![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > syl6bir | GIF 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 158 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) |
3 | syl6bir.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 1800 cbvexdh 1926 repizf2 4159 issref 5007 fnun 5318 ovigg 5989 tfrlem9 6314 tfri3 6362 ordge1n0im 6431 nntri3or 6488 updjud 7075 axprecex 7870 peano5nnnn 7882 peano5nni 8911 zeo 9347 nn0ind-raph 9359 fzm1 10086 fzind2 10225 fzfig 10416 bcpasc 10730 climrecvg1n 11340 oddnn02np1 11868 oddge22np1 11869 evennn02n 11870 evennn2n 11871 gcdaddm 11968 coprmdvds1 12074 qredeq 12079 fiinopn 13169 zabsle1 14067 bj-intabssel 14197 triap 14433 |
Copyright terms: Public domain | W3C validator |