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 580 anandir 581 xchnxbi 670 orordi 763 orordir 764 sbco3v 1956 sbco4 1994 elsb3 2142 elsb4 2143 abeq1i 2276 cbvabw 2287 r19.41 2619 rexcom4a 2745 moeq 2896 mosubt 2898 2reuswapdc 2925 nfcdeq 2943 sbcid 2961 sbcco2 2968 sbc7 2972 sbcie2g 2979 eqsbc3 2985 sbcralt 3022 sbcrext 3023 cbvralcsf 3102 cbvrexcsf 3103 cbvrabcsf 3105 abss 3206 ssab 3207 difrab 3391 abn0m 3429 prsspw 3739 disjnim 3967 brab1 4023 unopab 4055 exss 4199 uniuni 4423 elvvv 4661 eliunxp 4737 ralxp 4741 rexxp 4742 opelco 4770 reldm0 4816 resieq 4888 resiexg 4923 iss 4924 imai 4954 cnvsym 4981 intasym 4982 asymref 4983 codir 4986 poirr2 4990 rninxp 5041 cnvsom 5141 funopg 5216 fin 5368 f1cnvcnv 5398 fndmin 5586 resoprab 5929 mpo2eqb 5942 ov6g 5970 offval 6051 dfopab2 6149 dfoprab3s 6150 fmpox 6160 spc2ed 6192 brtpos0 6211 dftpos3 6221 tpostpos 6223 ercnv 6513 xpcomco 6783 xpassen 6787 phpm 6822 ctssdccl 7067 elni2 7246 elfz2nn0 10037 elfzmlbp 10057 clim0 11212 isstructim 12351 ntreq0 12679 cnmptcom 12845 dedekindicclemicc 13157 |
Copyright terms: Public domain | W3C validator |