![]() |
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-1 5 ax-2 6 ax-mp 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 562 anandir 563 xchnxbi 652 orordi 745 orordir 746 sbco3v 1916 elsb3 1925 elsb4 1926 sbco4 1956 abeq1i 2224 r19.41 2558 rexcom4a 2679 moeq 2826 mosubt 2828 2reuswapdc 2855 nfcdeq 2873 sbcid 2891 sbcco2 2898 sbc7 2902 sbcie2g 2908 eqsbc3 2914 sbcralt 2951 sbcrext 2952 cbvralcsf 3026 cbvrexcsf 3027 cbvrabcsf 3029 abss 3130 ssab 3131 difrab 3314 abn0m 3352 prsspw 3656 disjnim 3884 brab1 3938 unopab 3965 exss 4107 uniuni 4330 elvvv 4560 eliunxp 4636 ralxp 4640 rexxp 4641 opelco 4669 reldm0 4715 resieq 4785 resiexg 4820 iss 4821 imai 4851 cnvsym 4878 intasym 4879 asymref 4880 codir 4883 poirr2 4887 rninxp 4938 cnvsom 5038 funopg 5113 fin 5265 f1cnvcnv 5295 fndmin 5479 resoprab 5819 mpo2eqb 5832 ov6g 5860 offval 5941 dfopab2 6039 dfoprab3s 6040 fmpox 6050 spc2ed 6082 brtpos0 6101 dftpos3 6111 tpostpos 6113 ercnv 6402 xpcomco 6671 xpassen 6675 phpm 6710 ctssdccl 6946 elni2 7064 elfz2nn0 9779 elfzmlbp 9796 clim0 10940 isstructim 11810 ntreq0 12138 cnmptcom 12303 |
Copyright terms: Public domain | W3C validator |