![]() |
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 158 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) |
3 | sylbird.2 | . 2 ⊢ (𝜑 → (𝜒 → 𝜃)) | |
4 | 2, 3 | syld 45 | 1 ⊢ (𝜑 → (𝜓 → 𝜃)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 105 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: 3imtr3d 202 drex1 1798 eqreu 2931 onsucsssucr 4510 ordsucunielexmid 4532 ovi3 6013 tfrlem9 6322 dom2lem 6774 distrlem4prl 7585 distrlem4pru 7586 recexprlemm 7625 caucvgprlem1 7680 caucvgprprlemexb 7708 aptisr 7780 map2psrprg 7806 renegcl 8220 addid0 8332 remulext2 8559 mulext1 8571 apmul1 8747 nnge1 8944 0mnnnnn0 9210 nn0lt2 9336 zneo 9356 uzind2 9367 fzind 9370 nn0ind-raph 9372 ledivge1le 9728 elfzmlbp 10134 difelfznle 10137 elfzodifsumelfzo 10203 ssfzo12 10226 flqeqceilz 10320 addmodlteq 10400 uzsinds 10444 qsqeqor 10633 facdiv 10720 facwordi 10722 bcpasc 10748 addcn2 11320 mulcn2 11322 climrecvg1n 11358 odd2np1 11880 oddge22np1 11888 gcdaddm 11987 algcvgblem 12051 cncongr1 12105 pcdvdsb 12321 pcaddlem 12340 infpnlem1 12359 prmunb 12362 imasaddfnlemg 12740 subrgdvds 13361 aprcotr 13380 metss2lem 14082 lgseisenlem2 14536 2sqlem6 14552 |
Copyright terms: Public domain | W3C validator |