![]() |
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 119 | . 2 ⊢ (𝜑 → 𝜓) |
3 | sylanb.2 | . 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃) | |
4 | 2, 3 | sylan 278 | 1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: syl2anb 286 anabsan 543 2exeu 2047 eqtr2 2113 pm13.181 2344 rmob 2945 disjne 3355 seex 4186 tron 4233 fssres 5221 funbrfvb 5382 funopfvb 5383 fvelrnb 5387 fvco 5409 fvimacnvi 5452 ffvresb 5500 funresdfunsnss 5539 fvtp2g 5545 fvtp2 5548 fnex 5558 funex 5559 1st2nd 5989 dftpos4 6066 nnmsucr 6289 nnmcan 6318 xpmapenlem 6645 fundmfibi 6728 sup3exmid 8515 nzadd 8900 peano5uzti 8953 fnn0ind 8961 uztrn2 9135 irradd 9230 xltnegi 9401 xaddnemnf 9423 xaddnepnf 9424 xaddcom 9427 xnegdi 9434 elioore 9478 uzsubsubfz1 9611 fzo1fzo0n0 9743 elfzonelfzo 9790 qbtwnxr 9818 faclbnd 10280 faclbnd3 10282 dvdsprime 11547 restuni 12040 stoig 12041 cnnei 12099 tgioo 12336 bj-indind 12551 |
Copyright terms: Public domain | W3C validator |