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-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: dcnnOLD 819 excxor 1341 sbequ8 1803 2sb5 1936 2sb6 1937 2sb5rf 1942 2sb6rf 1943 moabs 2026 moanim 2051 2eu4 2070 2eu7 2071 sb8ab 2239 risset 2440 reuind 2862 difundi 3298 indifdir 3302 unab 3313 inab 3314 rabeq0 3362 abeq0 3363 inssdif0im 3400 snprc 3558 snss 3619 unipr 3720 uni0b 3731 pwtr 4111 opm 4126 onintexmid 4457 elxp2 4527 opthprc 4560 xpiundir 4568 elvvv 4572 relun 4626 inopab 4641 difopab 4642 ralxpf 4655 rexxpf 4656 dmiun 4718 rniun 4919 cnvresima 4998 imaco 5014 fnopabg 5216 dff1o2 5340 idref 5626 imaiun 5629 opabex3d 5987 opabex3 5988 elixx3g 9652 elfz2 9765 elfzuzb 9768 divalgb 11549 1nprm 11722 alsconv 13173 |
Copyright terms: Public domain | W3C validator |