![]() |
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 144 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) |
3 | syl6bi.2 | . 2 ⊢ (𝜒 → 𝜃) | |
4 | 2, 3 | syl6 33 | 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 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: 19.33bdc 1630 ax11i 1714 equveli 1759 eupickbi 2108 nfabdw 2338 rgen2a 2531 reu6 2926 sseq0 3464 disjel 3477 preq12b 3768 prel12 3769 prneimg 3772 elinti 3851 exmidundif 4203 opthreg 4551 elreldm 4848 issref 5006 relcnvtr 5143 relresfld 5153 funopg 5245 funimass2 5289 f0dom0 5404 fvimacnv 5626 elunirn 5760 oprabid 5900 op1steq 6173 f1o2ndf1 6222 reldmtpos 6247 rntpos 6251 nntri3or 6487 nnaordex 6522 nnawordex 6523 findcard2 6882 findcard2s 6883 mkvprop 7149 cc2lem 7243 lt2addnq 7381 lt2mulnq 7382 genpelvl 7489 genpelvu 7490 distrlem5prl 7563 distrlem5pru 7564 caucvgprlemnkj 7643 map2psrprg 7782 rereceu 7866 ltxrlt 8000 0mnnnnn0 9184 elnnnn0b 9196 nn0le2is012 9311 btwnz 9348 uz11 9526 nn01to3 9593 zq 9602 xrltso 9770 xltnegi 9809 xnn0lenn0nn0 9839 xnn0xadd0 9841 iccleub 9905 fzdcel 10013 uznfz 10076 2ffzeq 10114 elfzonlteqm1 10183 icogelb 10239 flqeqceilz 10291 modqadd1 10334 modqmul1 10350 frecuzrdgtcl 10385 frecuzrdgfunlem 10392 fzfig 10403 m1expeven 10540 qsqeqor 10603 caucvgrelemcau 10960 rexico 11201 fisumss 11371 fsum2dlemstep 11413 ntrivcvgap 11527 fprodssdc 11569 fprod2dlemstep 11601 0dvds 11789 alzdvds 11830 opoe 11870 omoe 11871 opeo 11872 omeo 11873 m1exp1 11876 nn0enne 11877 nn0o1gt2 11880 gcdneg 11953 dfgcd2 11985 algcvgblem 12019 algcvga 12021 eucalglt 12027 coprmdvds 12062 divgcdcoprmex 12072 cncongr1 12073 prm2orodd 12096 prm23lt5 12233 pockthi 12326 ismnddef 12698 tg2 13193 tgcl 13197 neii1 13280 neii2 13282 txlm 13412 reopnap 13671 tgioo 13679 addcncntoplem 13684 bj-elssuniab 14165 bj-nn0sucALT 14352 triap 14400 |
Copyright terms: Public domain | W3C validator |