![]() |
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 187 | . 2 ⊢ (𝜑 ↔ 𝜃) |
5 | 1, 4 | bitr2i 185 | 1 ⊢ (𝜃 ↔ 𝜒) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 105 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: dcnnOLD 849 excxor 1378 sbequ8 1847 2sb5 1983 2sb6 1984 2sb5rf 1989 2sb6rf 1990 moabs 2075 moanim 2100 2eu4 2119 2eu7 2120 sb8ab 2299 risset 2505 cbvreuvw 2711 reuind 2944 difundi 3389 indifdir 3393 unab 3404 inab 3405 rabeq0 3454 abeq0 3455 inssdif0im 3492 snprc 3659 snssOLD 3720 unipr 3825 uni0b 3836 pwtr 4221 opm 4236 onintexmid 4574 elxp2 4646 opthprc 4679 xpiundir 4687 elvvv 4691 relun 4745 inopab 4761 difopab 4762 ralxpf 4775 rexxpf 4776 dmiun 4838 rniun 5041 cnvresima 5120 imaco 5136 fnopabg 5341 dff1o2 5468 idref 5759 imaiun 5763 opabex3d 6124 opabex3 6125 onntri35 7238 elixx3g 9903 elfz2 10017 elfzuzb 10021 divalgb 11932 1nprm 12116 issubg3 13057 alsconv 14867 |
Copyright terms: Public domain | W3C validator |