![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3bitr4ri | GIF version |
Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 2-Sep-1995.) |
Ref | Expression |
---|---|
3bitr4i.1 | ⊢ (𝜑 ↔ 𝜓) |
3bitr4i.2 | ⊢ (𝜒 ↔ 𝜑) |
3bitr4i.3 | ⊢ (𝜃 ↔ 𝜓) |
Ref | Expression |
---|---|
3bitr4ri | ⊢ (𝜃 ↔ 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3bitr4i.2 | . 2 ⊢ (𝜒 ↔ 𝜑) | |
2 | 3bitr4i.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
3 | 3bitr4i.3 | . . 3 ⊢ (𝜃 ↔ 𝜓) | |
4 | 2, 3 | bitr4i 186 | . 2 ⊢ (𝜑 ↔ 𝜃) |
5 | 1, 4 | bitr2i 184 | 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: dcnnOLD 817 excxor 1339 sbequ8 1801 2sb5 1934 2sb6 1935 2sb5rf 1940 2sb6rf 1941 moabs 2024 moanim 2049 2eu4 2068 2eu7 2069 sb8ab 2236 risset 2437 reuind 2858 difundi 3294 indifdir 3298 unab 3309 inab 3310 rabeq0 3358 abeq0 3359 inssdif0im 3396 snprc 3554 snss 3615 unipr 3716 uni0b 3727 pwtr 4101 opm 4116 onintexmid 4447 elxp2 4517 opthprc 4550 xpiundir 4558 elvvv 4562 relun 4616 inopab 4631 difopab 4632 ralxpf 4645 rexxpf 4646 dmiun 4708 rniun 4907 cnvresima 4986 imaco 5002 fnopabg 5204 dff1o2 5328 idref 5612 imaiun 5615 opabex3d 5973 opabex3 5974 elixx3g 9577 elfz2 9690 elfzuzb 9693 divalgb 11470 1nprm 11641 alsconv 12937 |
Copyright terms: Public domain | W3C validator |