Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3bitr3i | Structured version Visualization version GIF version |
Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 19-Aug-1993.) |
Ref | Expression |
---|---|
3bitr3i.1 | ⊢ (𝜑 ↔ 𝜓) |
3bitr3i.2 | ⊢ (𝜑 ↔ 𝜒) |
3bitr3i.3 | ⊢ (𝜓 ↔ 𝜃) |
Ref | Expression |
---|---|
3bitr3i | ⊢ (𝜒 ↔ 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3bitr3i.2 | . . 3 ⊢ (𝜑 ↔ 𝜒) | |
2 | 3bitr3i.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
3 | 1, 2 | bitr3i 265 | . 2 ⊢ (𝜒 ↔ 𝜓) |
4 | 3bitr3i.3 | . 2 ⊢ (𝜓 ↔ 𝜃) | |
5 | 3, 4 | bitri 263 | 1 ⊢ (𝜒 ↔ 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 196 |
This theorem is referenced by: an12 834 xorass 1460 cbval2 2267 cbvaldva 2269 sbco2d 2404 sbcom 2406 equsb3 2420 equsb3ALT 2421 elsb3 2422 elsb4 2423 sb7f 2441 sbco4lem 2453 eq2tri 2671 eqsb3 2715 clelsb3 2716 r19.35 3065 ralcom4 3197 rexcom4 3198 ceqsralt 3202 gencbvex 3223 gencbval 3225 ceqsrexbv 3307 euind 3360 reuind 3378 sbccomlem 3475 sbccom 3476 csbcom 3946 difcom 4005 eqsn 4301 uniintsn 4449 disjxun 4581 reusv2lem4 4798 exss 4858 elxp2OLD 5057 eqbrriv 5138 dm0rn0 5263 dfres2 5372 qfto 5436 rninxp 5492 coeq0 5561 fununi 5878 dffv2 6181 fndmin 6232 fnprb 6377 fntpb 6378 dfoprab2 6599 dfer2 7630 eceqoveq 7740 euen1 7912 xpsnen 7929 xpassen 7939 marypha2lem3 8226 rankuni 8609 card1 8677 alephislim 8789 dfacacn 8846 kmlem4 8858 ac6num 9184 zorn2lem4 9204 fpwwe2lem8 9338 fpwwe2lem12 9342 mappsrpr 9808 sqeqori 12838 trclublem 13582 fprodle 14566 vdwmc2 15521 txflf 21620 metustid 22169 caucfil 22889 ovolgelb 23055 dfcgra2 25521 axcontlem5 25648 nmoubi 27011 hvsubaddi 27307 hlimeui 27481 omlsilem 27645 pjoml3i 27829 hodsi 28018 nmopub 28151 nmfnleub 28168 nmopcoadj0i 28346 pjin3i 28437 or3dir 28692 ralcom4f 28700 rexcom4f 28701 clelsb3f 28704 uniinn0 28749 ordtconlem1 29298 bnj62 30040 bnj610 30071 bnj1143 30115 bnj1533 30176 bnj543 30217 bnj545 30219 bnj594 30236 ceqsralv2 30862 br1steq 30917 br2ndeq 30918 brsuccf 31218 brfullfun 31225 filnetlem4 31546 bj-ssbcom3lem 31839 bj-cbval2v 31924 bj-clelsb3 32042 icorempt2 32375 poimirlem13 32592 poimirlem14 32593 poimirlem21 32600 poimirlem22 32601 poimir 32612 sbccom2lem 33099 isltrn2N 34424 moxfr 36273 ifporcor 36825 ifpancor 36827 ifpbicor 36839 ifpnorcor 36844 ifpnancor 36845 ifpororb 36869 relexp0eq 37012 hashnzfzclim 37543 pm11.6 37614 sbc3or 37759 cbvexsv 37783 frgr3v 41445 copisnmnd 41599 |
Copyright terms: Public domain | W3C validator |