![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > syl6rbbr | GIF version |
Description: A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.) |
Ref | Expression |
---|---|
syl6rbbr.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
syl6rbbr.2 | ⊢ (𝜃 ↔ 𝜒) |
Ref | Expression |
---|---|
syl6rbbr | ⊢ (𝜑 → (𝜃 ↔ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl6rbbr.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | syl6rbbr.2 | . . 3 ⊢ (𝜃 ↔ 𝜒) | |
3 | 2 | bicomi 123 | . 2 ⊢ (𝜒 ↔ 𝜃) |
4 | 1, 3 | syl6rbb 186 | 1 ⊢ (𝜑 → (𝜃 ↔ 𝜓)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 98 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: imimorbdc 795 baib 828 pm5.6dc 835 xornbidc 1282 mo2dc 1955 reu8 2737 sbc6g 2788 r19.28m 3311 r19.45mv 3315 r19.27m 3316 ralsnsg 3407 ralsns 3408 rexsnsOLD 3410 iunconstm 3665 iinconstm 3666 unisucg 4151 funssres 4942 fncnv 4965 dff1o5 5135 funimass4 5224 fneqeql2 5276 fnniniseg2 5290 rexsupp 5291 unpreima 5292 dffo3 5314 funfvima 5390 dff13 5407 f1eqcocnv 5431 fliftf 5439 isocnv2 5452 eloprabga 5591 mpt22eqb 5610 opabex3d 5748 opabex3 5749 elxp6 5796 elxp7 5797 genpdflem 6605 ltnqpr 6691 ltexprlemloc 6705 xrlenlt 7084 negcon2 7264 elznn 8261 zq 8561 rpnegap 8615 shftdm 9423 rexanuz2 9589 |
Copyright terms: Public domain | W3C validator |