Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3eqtri | Unicode version |
Description: An inference from three chained equalities. (Contributed by NM, 29-Aug-1993.) |
Ref | Expression |
---|---|
3eqtri.1 | |
3eqtri.2 | |
3eqtri.3 |
Ref | Expression |
---|---|
3eqtri |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3eqtri.1 | . 2 | |
2 | 3eqtri.2 | . . 3 | |
3 | 3eqtri.3 | . . 3 | |
4 | 2, 3 | eqtri 2158 | . 2 |
5 | 1, 4 | eqtri 2158 | 1 |
Colors of variables: wff set class |
Syntax hints: wceq 1331 |
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 1423 ax-gen 1425 ax-4 1487 ax-17 1506 ax-ext 2119 |
This theorem depends on definitions: df-bi 116 df-cleq 2130 |
This theorem is referenced by: csbid 3006 un23 3230 in32 3283 dfrab2 3346 difun2 3437 tpidm23 3619 unisn 3747 dfiunv2 3844 uniop 4172 suc0 4328 unisuc 4330 iunsuc 4337 xpun 4595 dfrn2 4722 dfdmf 4727 dfrnf 4775 res0 4818 resres 4826 xpssres 4849 dfima2 4878 imai 4890 ima0 4893 imaundir 4947 xpima1 4980 xpima2m 4981 dmresv 4992 rescnvcnv 4996 dmtpop 5009 rnsnopg 5012 resdmres 5025 dmmpt 5029 dmco 5042 co01 5048 fpr 5595 fmptpr 5605 fvsnun2 5611 mpo0 5834 dmoprab 5845 rnoprab 5847 ov6g 5901 1st0 6035 2nd0 6036 dfmpo 6113 algrflem 6119 dftpos2 6151 tposoprab 6170 tposmpo 6171 tfrlem8 6208 frecsuc 6297 df2o3 6320 sbthlemi5 6842 sup00 6883 casedm 6964 djudm 6983 axi2m1 7676 2p2e4 8840 numsuc 9188 numsucc 9214 decmul10add 9243 5p5e10 9245 6p4e10 9246 7p3e10 9249 xnegmnf 9605 pnfaddmnf 9626 fz0tp 9894 fzo0to2pr 9988 fzo0to3tp 9989 fzo0to42pr 9990 0tonninf 10205 1tonninf 10206 inftonninf 10207 sq4e2t8 10383 i4 10388 fac1 10468 fac3 10471 abs0 10823 absi 10824 trirecip 11263 geoihalfsum 11284 esum 11357 tan0 11427 ef01bndlem 11452 3dvdsdec 11551 3dvds2dec 11552 3lcm2e6woprm 11756 6lcm4e12 11757 ennnfonelem1 11909 ndxarg 11971 setsfun 11983 setsfun0 11984 txbasval 12425 cnmpt1st 12446 cnmpt2nd 12447 dvmptidcn 12836 cos2pi 12874 tan4thpi 12911 sincos6thpi 12912 pwf1oexmid 13183 isomninnlem 13214 |
Copyright terms: Public domain | W3C validator |