Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > syl6bi | GIF version |
Description: A mixed syllogism inference. (Contributed by NM, 2-Jan-1994.) |
Ref | Expression |
---|---|
syl6bi.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
syl6bi.2 | ⊢ (𝜒 → 𝜃) |
Ref | Expression |
---|---|
syl6bi | ⊢ (𝜑 → (𝜓 → 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl6bi.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | 1 | biimpd 142 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) |
3 | syl6bi.2 | . 2 ⊢ (𝜒 → 𝜃) | |
4 | 2, 3 | syl6 33 | 1 ⊢ (𝜑 → (𝜓 → 𝜃)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 103 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: 19.33bdc 1561 ax11i 1642 equveli 1682 eupickbi 2023 rgen2a 2417 reu6 2781 sseq0 3285 disjel 3298 preq12b 3562 prel12 3563 prneimg 3566 elinti 3645 opthreg 4299 elreldm 4578 issref 4727 relcnvtr 4860 relresfld 4867 funopg 4954 funimass2 4997 fvimacnv 5303 elunirn 5426 oprabid 5557 op1steq 5825 f1o2ndf1 5869 reldmtpos 5891 rntpos 5895 nntri3or 6095 nnaordex 6123 nnawordex 6124 findcard2 6373 findcard2s 6374 lt2addnq 6594 lt2mulnq 6595 genpelvl 6702 genpelvu 6703 distrlem5prl 6776 distrlem5pru 6777 caucvgprlemnkj 6856 rereceu 7055 ltxrlt 7178 0mnnnnn0 8320 elnnnn0b 8332 btwnz 8466 uz11 8641 nn01to3 8702 zq 8711 xrltso 8871 xltnegi 8902 iccleub 8954 fzdcel 9059 uznfz 9120 2ffzeq 9151 elfzonlteqm1 9219 flqeqceilz 9320 modqadd1 9363 modqmul1 9379 frecuzrdgfn 9414 fzfig 9422 m1expeven 9523 caucvgrelemcau 9866 rexico 10107 0dvds 10215 alzdvds 10254 opoe 10295 omoe 10296 opeo 10297 omeo 10298 m1exp1 10301 nn0enne 10302 nn0o1gt2 10305 gcdneg 10373 dfgcd2 10403 algcvgblem 10431 ialgcvga 10433 eucalglt 10439 coprmdvds 10474 divgcdcoprmex 10484 cncongr1 10485 prm2orodd 10508 bj-elssuniab 10601 bj-nn0sucALT 10773 |
Copyright terms: Public domain | W3C validator |