Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3bitr3d | GIF version |
Description: Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula. (Contributed by NM, 24-Apr-1996.) |
Ref | Expression |
---|---|
3bitr3d.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
3bitr3d.2 | ⊢ (𝜑 → (𝜓 ↔ 𝜃)) |
3bitr3d.3 | ⊢ (𝜑 → (𝜒 ↔ 𝜏)) |
Ref | Expression |
---|---|
3bitr3d | ⊢ (𝜑 → (𝜃 ↔ 𝜏)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3bitr3d.2 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜃)) | |
2 | 3bitr3d.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
3 | 1, 2 | bitr3d 189 | . 2 ⊢ (𝜑 → (𝜃 ↔ 𝜒)) |
4 | 3bitr3d.3 | . 2 ⊢ (𝜑 → (𝜒 ↔ 𝜏)) | |
5 | 3, 4 | bitrd 187 | 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: csbcomg 3020 eloprabga 5851 ereldm 6465 mapen 6733 ordiso2 6913 subcan 8010 conjmulap 8482 ltrec 8634 divelunit 9778 fseq1m1p1 9868 fzm1 9873 fihashneq0 10534 hashfacen 10572 cvg1nlemcau 10749 lenegsq 10860 dvdsmod 11549 bezoutlemle 11685 rpexp 11820 qnumdenbi 11859 bdxmet 12659 txmetcnp 12676 cnmet 12688 |
Copyright terms: Public domain | W3C validator |