![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > syl5rbb | GIF version |
Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
syl5rbb.1 | ⊢ (φ ↔ ψ) |
syl5rbb.2 | ⊢ (χ → (ψ ↔ θ)) |
Ref | Expression |
---|---|
syl5rbb | ⊢ (χ → (θ ↔ φ)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl5rbb.1 | . . 3 ⊢ (φ ↔ ψ) | |
2 | syl5rbb.2 | . . 3 ⊢ (χ → (ψ ↔ θ)) | |
3 | 1, 2 | syl5bb 181 | . 2 ⊢ (χ → (φ ↔ θ)) |
4 | 3 | bicomd 129 | 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: syl5rbbr 184 pm5.17dc 809 dn1dc 866 csbabg 2901 uniiunlem 3022 inimasn 4684 cnvpom 4803 fnresdisj 4952 f1oiso 5408 reldm 5754 1idprl 6566 1idpru 6567 nndiv 7735 fzn 8676 fz1sbc 8728 bj-indeq 9388 |
Copyright terms: Public domain | W3C validator |