Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > sylanb | GIF version |
Description: A syllogism inference. (Contributed by NM, 18-May-1994.) |
Ref | Expression |
---|---|
sylanb.1 | ⊢ (𝜑 ↔ 𝜓) |
sylanb.2 | ⊢ ((𝜓 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
sylanb | ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylanb.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
2 | 1 | biimpi 113 | . 2 ⊢ (𝜑 → 𝜓) |
3 | sylanb.2 | . 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃) | |
4 | 2, 3 | sylan 267 | 1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 ↔ wb 98 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: syl2anb 275 anabsan 509 2exeu 1992 eqtr2 2058 pm13.181 2287 rmob 2850 disjne 3273 seex 4072 tron 4119 fssres 5066 funbrfvb 5216 funopfvb 5217 fvelrnb 5221 fvco 5243 fvimacnvi 5281 ffvresb 5328 fvtp2g 5370 fvtp2 5373 fnex 5383 funex 5384 1st2nd 5807 dftpos4 5878 nnmsucr 6067 nnmcan 6092 peano5uzti 8346 fnn0ind 8354 uztrn2 8490 irradd 8580 xltnegi 8748 elioore 8781 uzsubsubfz1 8912 fzo1fzo0n0 9039 elfzonelfzo 9086 bj-indind 10056 |
Copyright terms: Public domain | W3C validator |