Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > bitr2i | GIF version |
Description: An inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
bitr2i.1 | ⊢ (𝜑 ↔ 𝜓) |
bitr2i.2 | ⊢ (𝜓 ↔ 𝜒) |
Ref | Expression |
---|---|
bitr2i | ⊢ (𝜒 ↔ 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bitr2i.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
2 | bitr2i.2 | . . 3 ⊢ (𝜓 ↔ 𝜒) | |
3 | 1, 2 | bitri 183 | . 2 ⊢ (𝜑 ↔ 𝜒) |
4 | 3 | bicomi 131 | 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: 3bitrri 206 3bitr2ri 208 3bitr4ri 212 nan 666 pm4.15 668 3or6 1286 sbal1yz 1954 2exsb 1962 moanim 2051 2eu4 2070 cvjust 2112 abbi 2231 sbc8g 2889 ss2rab 3143 unass 3203 unss 3220 undi 3294 difindiss 3300 notm0 3353 disj 3381 unopab 3977 eqvinop 4135 pwexb 4365 dmun 4716 reldm0 4727 dmres 4810 imadmrn 4861 ssrnres 4951 dmsnm 4974 coundi 5010 coundir 5011 cnvpom 5051 xpcom 5055 fun11 5160 fununi 5161 funcnvuni 5162 isarep1 5179 fsn 5560 fconstfvm 5606 eufnfv 5616 acexmidlem2 5739 eloprabga 5826 funoprabg 5838 ralrnmpo 5853 rexrnmpo 5854 oprabrexex2 5996 dfer2 6398 euen1b 6665 xpsnen 6683 rexuz3 10730 tgval2 12147 ssntr 12218 metrest 12602 sinhalfpilem 12799 |
Copyright terms: Public domain | W3C validator |