![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > bitr3di | GIF version |
Description: A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.) |
Ref | Expression |
---|---|
bitr3di.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
bitr3di.2 | ⊢ (𝜓 ↔ 𝜃) |
Ref | Expression |
---|---|
bitr3di | ⊢ (𝜑 → (𝜒 ↔ 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bitr3di.2 | . . 3 ⊢ (𝜓 ↔ 𝜃) | |
2 | 1 | bicomi 131 | . 2 ⊢ (𝜃 ↔ 𝜓) |
3 | bitr3di.1 | . 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-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: xordc 1371 sbal2 1998 eqsnm 3690 fnressn 5614 fressnfv 5615 eluniimadm 5674 genpassl 7356 genpassu 7357 1idprl 7422 1idpru 7423 axcaucvglemres 7731 negeq0 8040 muleqadd 8453 crap0 8740 addltmul 8980 fzrev 9895 modq0 10133 cjap0 10711 cjne0 10712 caucvgrelemrec 10783 lenegsq 10899 isumss 11192 fsumsplit 11208 sumsplitdc 11233 dvdsabseq 11581 oddennn 11941 metrest 12714 elabgf0 13155 |
Copyright terms: Public domain | W3C validator |