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 147 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) |
3 | sylbird.2 | . 2 ⊢ (𝜑 → (𝜒 → 𝜃)) | |
4 | 2, 3 | syld 40 | 1 ⊢ (𝜑 → (𝜓 → 𝜃)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ 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: 3imtr3d 191 drex1 1679 eqreu 2733 onsucsssucr 4235 ordsucunielexmid 4256 ovi3 5637 tfrlem9 5935 rdgon 5973 dom2lem 6252 distrlem4prl 6682 distrlem4pru 6683 recexprlemm 6722 caucvgprlem1 6777 caucvgprprlemexb 6805 aptisr 6863 renegcl 7272 remulext2 7591 mulext1 7603 apmul1 7764 nnge1 7937 0mnnnnn0 8214 nn0lt2 8322 zneo 8339 uzind2 8350 fzind 8353 nn0ind-raph 8355 ledivge1le 8652 elfzmlbp 8990 difelfznle 8993 elfzodifsumelfzo 9057 ssfzo12 9080 flqeqceilz 9160 addcn2 9831 mulcn2 9833 climrecvg1n 9867 algcvgblem 9888 |
Copyright terms: Public domain | W3C validator |