Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > bitr3i | GIF version |
Description: An inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
bitr3i.1 | ⊢ (𝜓 ↔ 𝜑) |
bitr3i.2 | ⊢ (𝜓 ↔ 𝜒) |
Ref | Expression |
---|---|
bitr3i | ⊢ (𝜑 ↔ 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bitr3i.1 | . . 3 ⊢ (𝜓 ↔ 𝜑) | |
2 | 1 | bicomi 131 | . 2 ⊢ (𝜑 ↔ 𝜓) |
3 | bitr3i.2 | . 2 ⊢ (𝜓 ↔ 𝜒) | |
4 | 2, 3 | bitri 183 | 1 ⊢ (𝜑 ↔ 𝜒) |
Colors of variables: wff set class |
Syntax hints: ↔ 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: 3bitrri 206 3bitr3i 209 3bitr3ri 210 anandi 564 anandir 565 xchnxbi 654 orordi 747 orordir 748 sbco3v 1920 elsb3 1929 elsb4 1930 sbco4 1960 abeq1i 2229 r19.41 2563 rexcom4a 2684 moeq 2832 mosubt 2834 2reuswapdc 2861 nfcdeq 2879 sbcid 2897 sbcco2 2904 sbc7 2908 sbcie2g 2914 eqsbc3 2920 sbcralt 2957 sbcrext 2958 cbvralcsf 3032 cbvrexcsf 3033 cbvrabcsf 3035 abss 3136 ssab 3137 difrab 3320 abn0m 3358 prsspw 3662 disjnim 3890 brab1 3945 unopab 3977 exss 4119 uniuni 4342 elvvv 4572 eliunxp 4648 ralxp 4652 rexxp 4653 opelco 4681 reldm0 4727 resieq 4799 resiexg 4834 iss 4835 imai 4865 cnvsym 4892 intasym 4893 asymref 4894 codir 4897 poirr2 4901 rninxp 4952 cnvsom 5052 funopg 5127 fin 5279 f1cnvcnv 5309 fndmin 5495 resoprab 5835 mpo2eqb 5848 ov6g 5876 offval 5957 dfopab2 6055 dfoprab3s 6056 fmpox 6066 spc2ed 6098 brtpos0 6117 dftpos3 6127 tpostpos 6129 ercnv 6418 xpcomco 6688 xpassen 6692 phpm 6727 ctssdccl 6964 elni2 7090 elfz2nn0 9860 elfzmlbp 9877 clim0 11022 isstructim 11900 ntreq0 12228 cnmptcom 12394 dedekindicclemicc 12706 |
Copyright terms: Public domain | W3C validator |