![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3eqtr4g | Unicode version |
Description: A chained equality inference, useful for converting to definitions. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
3eqtr4g.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3eqtr4g.2 |
![]() ![]() ![]() ![]() |
3eqtr4g.3 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
3eqtr4g |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3eqtr4g.2 |
. . 3
![]() ![]() ![]() ![]() | |
2 | 3eqtr4g.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl5eq 2084 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3eqtr4g.3 |
. 2
![]() ![]() ![]() ![]() | |
5 | 3, 4 | syl6eqr 2090 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1336 ax-gen 1338 ax-4 1400 ax-17 1419 ax-ext 2022 |
This theorem depends on definitions: df-bi 110 df-cleq 2033 |
This theorem is referenced by: rabeqf 2550 csbeq1 2855 csbeq2d 2874 csbnestgf 2898 difeq1 3055 difeq2 3056 uneq2 3091 ineq2 3132 dfrab3ss 3215 ifeq1 3334 ifeq2 3335 ifbi 3348 pweq 3362 sneq 3386 csbsng 3431 rabsn 3437 preq1 3447 preq2 3448 tpeq1 3456 tpeq2 3457 tpeq3 3458 prprc1 3478 opeq1 3549 opeq2 3550 oteq1 3558 oteq2 3559 oteq3 3560 csbunig 3588 unieq 3589 inteq 3618 iineq1 3671 iineq2 3674 dfiin2g 3690 iinrabm 3719 iinin1m 3726 iinxprg 3731 opabbid 3822 mpteq12f 3837 suceq 4139 xpeq1 4359 xpeq2 4360 csbxpg 4421 csbdmg 4529 rneq 4561 reseq1 4606 reseq2 4607 csbresg 4615 resmpt 4656 imaeq1 4663 imaeq2 4664 csbrng 4782 dmpropg 4793 rnpropg 4800 cores 4824 cores2 4833 xpcom 4864 iotaeq 4875 iotabi 4876 fntpg 4955 funimaexg 4983 fveq1 5177 fveq2 5178 fvres 5198 csbfv12g 5209 fnimapr 5233 fndmin 5274 fprg 5346 fsnunfv 5363 fsnunres 5364 fliftf 5439 isoini2 5458 riotaeqdv 5469 riotabidv 5470 riotauni 5474 riotabidva 5484 snriota 5497 oveq 5518 oveq1 5519 oveq2 5520 oprabbid 5558 mpt2eq123 5564 mpt2eq123dva 5566 mpt2eq3dva 5569 resmpt2 5599 ovres 5640 f1ocnvd 5702 ofeq 5714 ofreq 5715 ovtposg 5874 recseq 5921 tfr2a 5936 rdgeq1 5958 rdgeq2 5959 freceq1 5979 freceq2 5980 eceq1 6141 eceq2 6143 qseq1 6154 qseq2 6155 uniqs 6164 ecinxp 6181 qsinxp 6182 erovlem 6198 addpiord 6414 mulpiord 6415 00sr 6854 negeq 7204 csbnegg 7209 negsubdi 7267 mulneg1 7392 deceq1 8370 deceq2 8371 xnegeq 8740 fseq1p1m1 8956 frec2uzzd 9186 frec2uzsucd 9187 frec2uzrdg 9195 frecuzrdgsuc 9201 iseqeq1 9214 iseqeq2 9215 iseqeq3 9216 iseqeq4 9217 shftdm 9423 resqrexlemfp1 9607 sumeq1 9874 |
Copyright terms: Public domain | W3C validator |