![]() |
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 1562 ax11i 1644 equveli 1684 eupickbi 2025 rgen2a 2423 reu6 2792 sseq0 3306 disjel 3319 preq12b 3588 prel12 3589 prneimg 3592 elinti 3671 exmidundif 3999 opthreg 4335 elreldm 4619 issref 4769 relcnvtr 4904 relresfld 4914 funopg 5001 funimass2 5045 f0dom0 5152 fvimacnv 5359 elunirn 5485 oprabid 5616 op1steq 5884 f1o2ndf1 5928 reldmtpos 5950 rntpos 5954 nntri3or 6186 nnaordex 6216 nnawordex 6217 findcard2 6535 findcard2s 6536 lt2addnq 6866 lt2mulnq 6867 genpelvl 6974 genpelvu 6975 distrlem5prl 7048 distrlem5pru 7049 caucvgprlemnkj 7128 rereceu 7327 ltxrlt 7455 0mnnnnn0 8597 elnnnn0b 8609 btwnz 8761 uz11 8936 nn01to3 8997 zq 9006 xrltso 9161 xltnegi 9192 iccleub 9244 fzdcel 9349 uznfz 9410 2ffzeq 9442 elfzonlteqm1 9510 flqeqceilz 9614 modqadd1 9657 modqmul1 9673 frecuzrdgtcl 9708 frecuzrdgfunlem 9715 fzfig 9726 m1expeven 9839 caucvgrelemcau 10240 rexico 10481 0dvds 10596 alzdvds 10635 opoe 10675 omoe 10676 opeo 10677 omeo 10678 m1exp1 10681 nn0enne 10682 nn0o1gt2 10685 gcdneg 10753 dfgcd2 10783 algcvgblem 10811 ialgcvga 10813 eucalglt 10819 coprmdvds 10854 divgcdcoprmex 10864 cncongr1 10865 prm2orodd 10888 bj-elssuniab 11034 bj-nn0sucALT 11216 |
Copyright terms: Public domain | W3C validator |