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 281 | 1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: syl2anb 289 anabsan 564 2exeu 2091 eqtr2 2158 pm13.181 2390 rmob 3001 disjne 3416 seex 4257 tron 4304 fssres 5298 funbrfvb 5464 funopfvb 5465 fvelrnb 5469 fvco 5491 fvimacnvi 5534 ffvresb 5583 funresdfunsnss 5623 fvtp2g 5629 fvtp2 5632 fnex 5642 funex 5643 1st2nd 6079 dftpos4 6160 nnmsucr 6384 nnmcan 6415 xpmapenlem 6743 fundmfibi 6827 sup3exmid 8715 nzadd 9106 peano5uzti 9159 fnn0ind 9167 uztrn2 9343 irradd 9438 xltnegi 9618 xaddnemnf 9640 xaddnepnf 9641 xaddcom 9644 xnegdi 9651 elioore 9695 uzsubsubfz1 9828 fzo1fzo0n0 9960 elfzonelfzo 10007 qbtwnxr 10035 faclbnd 10487 faclbnd3 10489 dvdsprime 11803 restuni 12341 stoig 12342 cnnei 12401 tgioo 12715 divcnap 12724 bj-indind 13130 |
Copyright terms: Public domain | W3C validator |