Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > sylbird | GIF version |
Description: A syllogism deduction. (Contributed by NM, 3-Aug-1994.) |
Ref | Expression |
---|---|
sylbird.1 | ⊢ (𝜑 → (𝜒 ↔ 𝜓)) |
sylbird.2 | ⊢ (𝜑 → (𝜒 → 𝜃)) |
Ref | Expression |
---|---|
sylbird | ⊢ (𝜑 → (𝜓 → 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylbird.1 | . . 3 ⊢ (𝜑 → (𝜒 ↔ 𝜓)) | |
2 | 1 | biimprd 157 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) |
3 | sylbird.2 | . 2 ⊢ (𝜑 → (𝜒 → 𝜃)) | |
4 | 2, 3 | syld 45 | 1 ⊢ (𝜑 → (𝜓 → 𝜃)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ 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: 3imtr3d 201 drex1 1770 eqreu 2871 onsucsssucr 4420 ordsucunielexmid 4441 ovi3 5900 tfrlem9 6209 dom2lem 6659 distrlem4prl 7385 distrlem4pru 7386 recexprlemm 7425 caucvgprlem1 7480 caucvgprprlemexb 7508 aptisr 7580 map2psrprg 7606 renegcl 8016 addid0 8128 remulext2 8355 mulext1 8367 apmul1 8541 nnge1 8736 0mnnnnn0 9002 nn0lt2 9125 zneo 9145 uzind2 9156 fzind 9159 nn0ind-raph 9161 ledivge1le 9506 elfzmlbp 9902 difelfznle 9905 elfzodifsumelfzo 9971 ssfzo12 9994 flqeqceilz 10084 addmodlteq 10164 uzsinds 10208 facdiv 10477 facwordi 10479 bcpasc 10505 addcn2 11072 mulcn2 11074 climrecvg1n 11110 odd2np1 11559 oddge22np1 11567 gcdaddm 11661 algcvgblem 11719 cncongr1 11773 metss2lem 12655 |
Copyright terms: Public domain | W3C validator |