![]() |
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 123 | . 2 ⊢ (φ ↔ ψ) |
3 | syl5rbbr.2 | . 2 ⊢ (χ → (ψ ↔ θ)) | |
4 | 2, 3 | syl5rbb 182 | 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: xordc 1280 sbal2 1895 eqsnm 3517 fnressn 5292 fressnfv 5293 eluniimadm 5347 genpassl 6507 genpassu 6508 1idprl 6566 1idpru 6567 negeq0 7061 muleqadd 7431 crap0 7691 addltmul 7938 fzrev 8716 cjap0 9135 cjne0 9136 elabgf0 9251 |
Copyright terms: Public domain | W3C validator |