![]() |
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 555 anandir 556 xchnxbi 638 orordi 723 orordir 724 sbco3v 1885 elsb3 1894 elsb4 1895 sbco4 1925 abeq1i 2191 r19.41 2510 rexcom4a 2624 moeq 2768 mosubt 2770 2reuswapdc 2795 nfcdeq 2813 sbcid 2831 sbcco2 2838 sbc7 2842 sbcie2g 2848 eqsbc3 2854 sbcralt 2891 sbcrext 2892 cbvralcsf 2965 cbvrexcsf 2966 cbvrabcsf 2968 abss 3064 ssab 3065 difrab 3245 prsspw 3565 brab1 3838 unopab 3865 exss 3990 uniuni 4209 elvvv 4429 eliunxp 4503 ralxp 4507 rexxp 4508 opelco 4535 reldm0 4581 resieq 4650 resiexg 4683 iss 4684 imai 4711 cnvsym 4738 intasym 4739 asymref 4740 codir 4743 poirr2 4747 rninxp 4794 cnvsom 4891 funopg 4964 fin 5107 f1cnvcnv 5131 fndmin 5306 resoprab 5628 mpt22eqb 5641 ov6g 5669 offval 5750 dfopab2 5846 dfoprab3s 5847 fmpt2x 5857 spc2ed 5885 brtpos0 5901 dftpos3 5911 tpostpos 5913 ercnv 6193 xpcomco 6370 xpassen 6374 phpm 6400 elni2 6566 elfz2nn0 9205 elfzmlbp 9220 clim0 10262 |
Copyright terms: Public domain | W3C validator |