![]() |
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 130 | . 2 ⊢ (𝜑 ↔ 𝜓) |
3 | syl5rbbr.2 | . 2 ⊢ (𝜒 → (𝜓 ↔ 𝜃)) | |
4 | 2, 3 | syl5rbb 191 | 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 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: xordc 1328 sbal2 1946 eqsnm 3599 fnressn 5483 fressnfv 5484 eluniimadm 5544 genpassl 7081 genpassu 7082 1idprl 7147 1idpru 7148 axcaucvglemres 7432 negeq0 7734 muleqadd 8135 crap0 8416 addltmul 8650 fzrev 9494 modq0 9732 cjap0 10337 cjne0 10338 caucvgrelemrec 10408 lenegsq 10524 isumss 10779 fsumsplit 10797 sumsplitdc 10822 dvdsabseq 11122 oddennn 11479 elabgf0 11632 |
Copyright terms: Public domain | W3C validator |