![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eqtr4i | Unicode version |
Description: An equality transitivity inference. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
eqtr4i.1 |
![]() ![]() ![]() ![]() |
eqtr4i.2 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
eqtr4i |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqtr4i.1 |
. 2
![]() ![]() ![]() ![]() | |
2 | eqtr4i.2 |
. . 3
![]() ![]() ![]() ![]() | |
3 | 2 | eqcomi 2181 |
. 2
![]() ![]() ![]() ![]() |
4 | 1, 3 | eqtri 2198 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-gen 1449 ax-4 1510 ax-17 1526 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-cleq 2170 |
This theorem is referenced by: 3eqtr2i 2204 3eqtr2ri 2205 3eqtr4i 2208 3eqtr4ri 2209 rabab 2758 cbvralcsf 3119 cbvrexcsf 3120 cbvrabcsf 3122 dfin5 3136 dfdif2 3137 uneqin 3386 unrab 3406 inrab 3407 inrab2 3408 difrab 3409 dfrab3ss 3413 rabun2 3414 difidALT 3492 difdifdirss 3507 dfif3 3547 tpidm 3694 dfint2 3846 iunrab 3934 uniiun 3940 intiin 3941 0iin 3945 mptv 4100 xpundi 4682 xpundir 4683 resiun2 4927 resopab 4951 opabresid 4960 dfse2 5001 cnvun 5034 cnvin 5036 imaundir 5042 imainrect 5074 cnvcnv2 5082 cnvcnvres 5092 dmtpop 5104 rnsnopg 5107 rnco2 5136 dmco 5137 co01 5143 unidmrn 5161 dfdm2 5163 funimaexg 5300 dfmpt3 5338 mptun 5347 funcocnv2 5486 fnasrn 5694 fnasrng 5696 fpr 5698 fmptap 5706 riotav 5835 dmoprab 5955 rnoprab2 5958 mpov 5964 mpomptx 5965 abrexex2g 6120 abrexex2 6124 1stval2 6155 2ndval2 6156 fo1st 6157 fo2nd 6158 xp2 6173 dfoprab4f 6193 fmpoco 6216 tposmpo 6281 recsfval 6315 frecfnom 6401 freccllem 6402 frecfcllem 6404 frecsuclem 6406 df2o3 6430 o1p1e2 6468 ecqs 6596 qliftf 6619 erovlem 6626 mapsnf1o3 6696 ixp0x 6725 xpf1o 6843 djuunr 7064 dmaddpq 7377 dmmulpq 7378 enq0enq 7429 nqprlu 7545 m1p1sr 7758 m1m1sr 7759 caucvgsr 7800 dfcnqs 7839 3m1e2 9037 2p2e4 9044 3p2e5 9058 3p3e6 9059 4p2e6 9060 4p3e7 9061 4p4e8 9062 5p2e7 9063 5p3e8 9064 5p4e9 9065 6p2e8 9066 6p3e9 9067 7p2e9 9068 nn0supp 9226 nnzrab 9275 nn0zrab 9276 dec0u 9402 dec0h 9403 decsuc 9412 decsucc 9422 numma 9425 decma 9432 decmac 9433 decma2c 9434 decadd 9435 decaddc 9436 decmul1 9445 decmul1c 9446 decmul2c 9447 5p5e10 9452 6p4e10 9453 7p3e10 9456 8p2e10 9461 5t5e25 9484 6t6e36 9489 8t6e48 9500 nn0uz 9560 nnuz 9561 xaddcom 9859 ioomax 9946 iccmax 9947 ioopos 9948 ioorp 9949 fseq1p1m1 10091 fzo0to2pr 10215 fzo0to3tp 10216 frecfzennn 10423 irec 10616 sq10e99m1 10688 facnn 10702 fac0 10703 faclbnd2 10717 zfz1isolemsplit 10813 minmax 11233 xrminmax 11268 fisumrev2 11449 fsumparts 11473 fsumiun 11480 isumnn0nn 11496 fprod2d 11626 fprodle 11643 ege2le3 11674 cos1bnd 11762 efieq1re 11774 eirraplem 11779 phiprmpw 12216 unennn 12392 ennnfonelemjn 12397 qnnen 12426 strle1g 12559 tgrest 13562 uniretop 13918 dvexp 14068 dvef 14081 cospi 14114 sincos6thpi 14156 lgsdir2lem2 14323 bj-omind 14568 |
Copyright terms: Public domain | W3C validator |