![]() |
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-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: 3imtr3d 201 drex1 1733 eqreu 2821 onsucsssucr 4354 ordsucunielexmid 4375 ovi3 5819 tfrlem9 6122 dom2lem 6569 distrlem4prl 7240 distrlem4pru 7241 recexprlemm 7280 caucvgprlem1 7335 caucvgprprlemexb 7363 aptisr 7421 renegcl 7840 addid0 7948 remulext2 8174 mulext1 8186 apmul1 8352 nnge1 8543 0mnnnnn0 8803 nn0lt2 8926 zneo 8946 uzind2 8957 fzind 8960 nn0ind-raph 8962 ledivge1le 9302 elfzmlbp 9692 difelfznle 9695 elfzodifsumelfzo 9761 ssfzo12 9784 flqeqceilz 9874 addmodlteq 9954 uzsinds 9997 facdiv 10261 facwordi 10263 bcpasc 10289 addcn2 10853 mulcn2 10855 climrecvg1n 10891 odd2np1 11300 oddge22np1 11308 gcdaddm 11402 algcvgblem 11458 cncongr1 11512 metss2lem 12283 |
Copyright terms: Public domain | W3C validator |