Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3eqtr4i | Unicode version |
Description: An inference from three chained equalities. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
Ref | Expression |
---|---|
3eqtr4i.1 | |
3eqtr4i.2 | |
3eqtr4i.3 |
Ref | Expression |
---|---|
3eqtr4i |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3eqtr4i.2 | . 2 | |
2 | 3eqtr4i.3 | . . 3 | |
3 | 3eqtr4i.1 | . . 3 | |
4 | 2, 3 | eqtr4i 2188 | . 2 |
5 | 1, 4 | eqtr4i 2188 | 1 |
Colors of variables: wff set class |
Syntax hints: wceq 1342 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1434 ax-gen 1436 ax-4 1497 ax-17 1513 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-cleq 2157 |
This theorem is referenced by: rabswap 2642 rabbiia 2706 cbvrab 2719 cbvcsbw 3044 cbvcsb 3045 csbco 3050 csbcow 3051 cbvrabcsf 3105 un4 3277 in13 3330 in31 3331 in4 3333 indifcom 3363 indir 3366 undir 3367 notrab 3394 dfnul3 3407 rab0 3432 prcom 3646 tprot 3663 tpcoma 3664 tpcomb 3665 tpass 3666 qdassr 3668 pw0 3714 opid 3770 int0 3832 cbviun 3897 cbviin 3898 iunrab 3907 iunin1 3924 cbvopab 4047 cbvopab1 4049 cbvopab2 4050 cbvopab1s 4051 cbvopab2v 4053 unopab 4055 cbvmptf 4070 cbvmpt 4071 iunopab 4253 uniuni 4423 2ordpr 4495 rabxp 4635 fconstmpt 4645 inxp 4732 cnvco 4783 rnmpt 4846 resundi 4891 resundir 4892 resindi 4893 resindir 4894 rescom 4903 resima 4911 imadmrn 4950 cnvimarndm 4962 cnvi 5002 rnun 5006 imaundi 5010 cnvxp 5016 imainrect 5043 imacnvcnv 5062 resdmres 5089 imadmres 5090 mptpreima 5091 cbviota 5152 sb8iota 5154 resdif 5448 cbvriota 5802 dfoprab2 5880 cbvoprab1 5905 cbvoprab2 5906 cbvoprab12 5907 cbvoprab3 5909 cbvmpox 5911 resoprab 5929 caov32 6020 caov31 6022 ofmres 6096 dfopab2 6149 dfxp3 6154 dmmpossx 6159 fmpox 6160 tposco 6234 mapsncnv 6652 cbvixp 6672 xpcomco 6783 sbthlemi6 6918 xp2dju 7162 djuassen 7164 dmaddpi 7257 dmmulpi 7258 dfplpq2 7286 dfmpq2 7287 dmaddpq 7311 dmmulpq 7312 axi2m1 7807 negiso 8841 nummac 9357 decsubi 9375 9t11e99 9442 fzprval 10007 fztpval 10008 sqdivapi 10528 binom2i 10553 4bc2eq6 10676 shftidt2 10760 cji 10830 xrnegiso 11189 cbvsum 11287 fsumrelem 11398 cbvprod 11485 nn0gcdsq 12111 restco 12721 cnmptid 12828 sincos3rdpi 13311 if0ab 13528 |
Copyright terms: Public domain | W3C validator |