![]() |
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 120 | . 2 ⊢ (𝜑 → 𝜓) |
3 | sylanb.2 | . 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃) | |
4 | 2, 3 | sylan 283 | 1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ↔ 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: syl2anb 291 anabsan 575 2exeu 2129 eqtr2 2207 pm13.181 2441 rmob 3069 disjne 3490 seex 4349 tron 4396 fssres 5405 funbrfvb 5573 funopfvb 5574 fvelrnb 5578 fvco 5601 fvimacnvi 5645 ffvresb 5694 funresdfunsnss 5734 fvtp2g 5740 fvtp2 5743 fnex 5753 funex 5754 1st2nd 6199 dftpos4 6281 nnmsucr 6506 nnmcan 6537 xpmapenlem 6866 fundmfibi 6955 sup3exmid 8931 nzadd 9322 peano5uzti 9378 fnn0ind 9386 uztrn2 9562 irradd 9663 xltnegi 9852 xaddnemnf 9874 xaddnepnf 9875 xaddcom 9878 xnegdi 9885 elioore 9929 uzsubsubfz1 10065 fzo1fzo0n0 10200 elfzonelfzo 10247 qbtwnxr 10275 faclbnd 10738 faclbnd3 10740 dvdsprime 12139 pcgcd 12345 restuni 14055 stoig 14056 cnnei 14115 tgioo 14429 divcnap 14438 lgsdi 14821 bj-indind 15067 |
Copyright terms: Public domain | W3C validator |