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 2876 onsucsssucr 4425 ordsucunielexmid 4446 ovi3 5907 tfrlem9 6216 dom2lem 6666 distrlem4prl 7392 distrlem4pru 7393 recexprlemm 7432 caucvgprlem1 7487 caucvgprprlemexb 7515 aptisr 7587 map2psrprg 7613 renegcl 8023 addid0 8135 remulext2 8362 mulext1 8374 apmul1 8548 nnge1 8743 0mnnnnn0 9009 nn0lt2 9132 zneo 9152 uzind2 9163 fzind 9166 nn0ind-raph 9168 ledivge1le 9513 elfzmlbp 9909 difelfznle 9912 elfzodifsumelfzo 9978 ssfzo12 10001 flqeqceilz 10091 addmodlteq 10171 uzsinds 10215 facdiv 10484 facwordi 10486 bcpasc 10512 addcn2 11079 mulcn2 11081 climrecvg1n 11117 odd2np1 11570 oddge22np1 11578 gcdaddm 11672 algcvgblem 11730 cncongr1 11784 metss2lem 12666 |
Copyright terms: Public domain | W3C validator |