![]() |
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 1676 eqreu 2727 onsucsssucr 4200 ordsucunielexmid 4216 ovi3 5579 tfrlem9 5876 rdgon 5913 dom2lem 6188 distrlem4prl 6560 distrlem4pru 6561 recexprlemm 6596 caucvgprlem1 6650 aptisr 6705 renegcl 7068 remulext2 7384 mulext1 7396 apmul1 7546 nnge1 7718 0mnnnnn0 7990 nn0lt2 8098 zneo 8115 uzind2 8126 fzind 8129 nn0ind-raph 8131 elfzmlbp 8760 difelfznle 8763 elfzodifsumelfzo 8827 ssfzo12 8850 |
Copyright terms: Public domain | W3C validator |