![]() |
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 2198 |
. 2
![]() ![]() ![]() ![]() |
5 | 1, 4 | 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: csbid 3067 un23 3296 in32 3349 dfrab2 3412 difun2 3504 tpidm23 3695 unisn 3827 dfiunv2 3924 uniop 4257 suc0 4413 unisuc 4415 iunsuc 4422 xpun 4689 dfrn2 4817 dfdmf 4822 dfrnf 4870 res0 4913 resres 4921 xpssres 4944 dfima2 4974 imai 4986 ima0 4989 imaundir 5044 xpima1 5077 xpima2m 5078 dmresv 5089 rescnvcnv 5093 dmtpop 5106 rnsnopg 5109 resdmres 5122 dmmpt 5126 dmco 5139 co01 5145 fpr 5700 fmptpr 5710 fvsnun2 5716 mpo0 5947 dmoprab 5958 rnoprab 5960 ov6g 6014 1st0 6147 2nd0 6148 dfmpo 6226 algrflem 6232 dftpos2 6264 tposoprab 6283 tposmpo 6284 tfrlem8 6321 frecsuc 6410 df2o3 6433 sbthlemi5 6962 sup00 7004 casedm 7087 djudm 7106 axi2m1 7876 2p2e4 9048 numsuc 9399 numsucc 9425 decmul10add 9454 5p5e10 9456 6p4e10 9457 7p3e10 9460 xnegmnf 9831 pnfaddmnf 9852 fz0tp 10124 fz0to3un2pr 10125 fzo0to2pr 10220 fzo0to3tp 10221 fzo0to42pr 10222 0tonninf 10441 1tonninf 10442 inftonninf 10443 sq4e2t8 10620 i4 10625 fac1 10711 fac3 10714 abs0 11069 absi 11070 trirecip 11511 geoihalfsum 11532 esum 11672 tan0 11741 ef01bndlem 11766 3dvdsdec 11872 3dvds2dec 11873 3lcm2e6woprm 12088 6lcm4e12 12089 ennnfonelem1 12410 ndxarg 12487 setsfun 12499 setsfun0 12500 txbasval 13806 cnmpt1st 13827 cnmpt2nd 13828 dvmptidcn 14217 cos2pi 14264 tan4thpi 14301 sincos6thpi 14302 sqrt2cxp2logb9e3 14432 012of 14784 2o01f 14785 pwf1oexmid 14788 isomninnlem 14817 iswomninnlem 14836 ismkvnnlem 14839 |
Copyright terms: Public domain | W3C validator |