![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > syl5rbbr | GIF version |
Description: A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.) |
Ref | Expression |
---|---|
syl5rbbr.1 | ⊢ (𝜓 ↔ 𝜑) |
syl5rbbr.2 | ⊢ (𝜒 → (𝜓 ↔ 𝜃)) |
Ref | Expression |
---|---|
syl5rbbr | ⊢ (𝜒 → (𝜃 ↔ 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl5rbbr.1 | . . 3 ⊢ (𝜓 ↔ 𝜑) | |
2 | 1 | bicomi 131 | . 2 ⊢ (𝜑 ↔ 𝜓) |
3 | syl5rbbr.2 | . 2 ⊢ (𝜒 → (𝜓 ↔ 𝜃)) | |
4 | 2, 3 | syl5rbb 192 | 1 ⊢ (𝜒 → (𝜃 ↔ 𝜑)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: xordc 1329 sbal2 1947 eqsnm 3605 fnressn 5497 fressnfv 5498 eluniimadm 5558 genpassl 7144 genpassu 7145 1idprl 7210 1idpru 7211 axcaucvglemres 7495 negeq0 7797 muleqadd 8198 crap0 8479 addltmul 8713 fzrev 9559 modq0 9797 cjap0 10402 cjne0 10403 caucvgrelemrec 10473 lenegsq 10589 isumss 10844 fsumsplit 10862 sumsplitdc 10887 dvdsabseq 11187 oddennn 11544 elabgf0 11950 |
Copyright terms: Public domain | W3C validator |