![]() |
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 2210 |
. 2
![]() ![]() ![]() ![]() |
5 | 1, 4 | eqtri 2210 |
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 1458 ax-gen 1460 ax-4 1521 ax-17 1537 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-cleq 2182 |
This theorem is referenced by: csbid 3080 un23 3309 in32 3362 dfrab2 3425 difun2 3517 tpidm23 3708 unisn 3840 dfiunv2 3937 uniop 4273 suc0 4429 unisuc 4431 iunsuc 4438 xpun 4705 dfrn2 4833 dfdmf 4838 dfrnf 4886 res0 4929 resres 4937 xpssres 4960 dfima2 4990 imai 5002 ima0 5005 imaundir 5060 xpima1 5093 xpima2m 5094 dmresv 5105 rescnvcnv 5109 dmtpop 5122 rnsnopg 5125 resdmres 5138 dmmpt 5142 dmco 5155 co01 5161 fpr 5719 fmptpr 5729 fvsnun2 5735 mpo0 5966 dmoprab 5977 rnoprab 5979 ov6g 6034 1st0 6169 2nd0 6170 dfmpo 6248 algrflem 6254 dftpos2 6286 tposoprab 6305 tposmpo 6306 tfrlem8 6343 frecsuc 6432 df2o3 6455 sbthlemi5 6990 sup00 7032 casedm 7115 djudm 7134 axi2m1 7904 2p2e4 9076 numsuc 9427 numsucc 9453 decmul10add 9482 5p5e10 9484 6p4e10 9485 7p3e10 9488 xnegmnf 9859 pnfaddmnf 9880 fz0tp 10152 fz0to3un2pr 10153 fzo0to2pr 10248 fzo0to3tp 10249 fzo0to42pr 10250 0tonninf 10470 1tonninf 10471 inftonninf 10472 sq4e2t8 10649 i4 10654 fac1 10741 fac3 10744 abs0 11099 absi 11100 trirecip 11541 geoihalfsum 11562 esum 11702 tan0 11771 ef01bndlem 11796 3dvdsdec 11902 3dvds2dec 11903 3lcm2e6woprm 12118 6lcm4e12 12119 ennnfonelem1 12458 ndxarg 12535 setsfun 12547 setsfun0 12548 txbasval 14224 cnmpt1st 14245 cnmpt2nd 14246 dvmptidcn 14635 cos2pi 14682 tan4thpi 14719 sincos6thpi 14720 sqrt2cxp2logb9e3 14850 012of 15204 2o01f 15205 pwf1oexmid 15208 isomninnlem 15237 iswomninnlem 15256 ismkvnnlem 15259 |
Copyright terms: Public domain | W3C validator |