![]() |
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 130 | . 2 ⊢ (𝜑 ↔ 𝜓) |
3 | bitr3i.2 | . 2 ⊢ (𝜓 ↔ 𝜒) | |
4 | 2, 3 | bitri 182 | 1 ⊢ (𝜑 ↔ 𝜒) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 103 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: 3bitrri 205 3bitr3i 208 3bitr3ri 209 anandi 557 anandir 558 xchnxbi 640 orordi 725 orordir 726 sbco3v 1891 elsb3 1900 elsb4 1901 sbco4 1931 abeq1i 2199 r19.41 2522 rexcom4a 2643 moeq 2790 mosubt 2792 2reuswapdc 2819 nfcdeq 2837 sbcid 2855 sbcco2 2862 sbc7 2866 sbcie2g 2872 eqsbc3 2878 sbcralt 2915 sbcrext 2916 cbvralcsf 2990 cbvrexcsf 2991 cbvrabcsf 2993 abss 3090 ssab 3091 difrab 3273 abn0m 3308 prsspw 3609 disjnim 3836 brab1 3890 unopab 3917 exss 4054 uniuni 4273 elvvv 4501 eliunxp 4575 ralxp 4579 rexxp 4580 opelco 4608 reldm0 4654 resieq 4723 resiexg 4757 iss 4758 imai 4788 cnvsym 4815 intasym 4816 asymref 4817 codir 4820 poirr2 4824 rninxp 4874 cnvsom 4974 funopg 5048 fin 5197 f1cnvcnv 5227 fndmin 5406 resoprab 5741 mpt22eqb 5754 ov6g 5782 offval 5863 dfopab2 5959 dfoprab3s 5960 fmpt2x 5970 spc2ed 5998 brtpos0 6017 dftpos3 6027 tpostpos 6029 ercnv 6311 xpcomco 6540 xpassen 6544 phpm 6579 elni2 6871 elfz2nn0 9522 elfzmlbp 9539 clim0 10669 isstructim 11504 |
Copyright terms: Public domain | W3C validator |