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 2194 | . 2 |
5 | 1, 4 | eqtr4i 2194 | 1 |
Colors of variables: wff set class |
Syntax hints: wceq 1348 |
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 1440 ax-gen 1442 ax-4 1503 ax-17 1519 ax-ext 2152 |
This theorem depends on definitions: df-bi 116 df-cleq 2163 |
This theorem is referenced by: rabswap 2648 rabbiia 2715 cbvrab 2728 cbvcsbw 3053 cbvcsb 3054 csbco 3059 csbcow 3060 cbvrabcsf 3114 un4 3287 in13 3340 in31 3341 in4 3343 indifcom 3373 indir 3376 undir 3377 notrab 3404 dfnul3 3417 rab0 3442 prcom 3657 tprot 3674 tpcoma 3675 tpcomb 3676 tpass 3677 qdassr 3679 pw0 3725 opid 3781 int0 3843 cbviun 3908 cbviin 3909 iunrab 3918 iunin1 3935 cbvopab 4058 cbvopab1 4060 cbvopab2 4061 cbvopab1s 4062 cbvopab2v 4064 unopab 4066 cbvmptf 4081 cbvmpt 4082 iunopab 4264 uniuni 4434 2ordpr 4506 rabxp 4646 fconstmpt 4656 inxp 4743 cnvco 4794 rnmpt 4857 resundi 4902 resundir 4903 resindi 4904 resindir 4905 rescom 4914 resima 4922 imadmrn 4961 cnvimarndm 4973 cnvi 5013 rnun 5017 imaundi 5021 cnvxp 5027 imainrect 5054 imacnvcnv 5073 resdmres 5100 imadmres 5101 mptpreima 5102 cbviota 5163 sb8iota 5165 resdif 5462 cbvriota 5816 dfoprab2 5897 cbvoprab1 5922 cbvoprab2 5923 cbvoprab12 5924 cbvoprab3 5926 cbvmpox 5928 resoprab 5946 caov32 6037 caov31 6039 ofmres 6112 dfopab2 6165 dfxp3 6170 dmmpossx 6175 fmpox 6176 tposco 6251 mapsncnv 6669 cbvixp 6689 xpcomco 6800 sbthlemi6 6935 xp2dju 7179 djuassen 7181 dmaddpi 7274 dmmulpi 7275 dfplpq2 7303 dfmpq2 7304 dmaddpq 7328 dmmulpq 7329 axi2m1 7824 negiso 8858 nummac 9374 decsubi 9392 9t11e99 9459 fzprval 10025 fztpval 10026 sqdivapi 10546 binom2i 10571 4bc2eq6 10695 shftidt2 10783 cji 10853 xrnegiso 11212 cbvsum 11310 fsumrelem 11421 cbvprod 11508 nn0gcdsq 12141 restco 12927 cnmptid 13034 sincos3rdpi 13517 lgsdir2lem5 13686 if0ab 13800 |
Copyright terms: Public domain | W3C validator |