![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > syl6eq | Unicode version |
Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
syl6eq.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
syl6eq.2 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
syl6eq |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl6eq.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | syl6eq.2 |
. . 3
![]() ![]() ![]() ![]() | |
3 | 2 | a1i 9 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | eqtrd 2072 |
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: syl6req 2089 syl6eqr 2090 3eqtr3g 2095 3eqtr4a 2098 cbvralcsf 2908 cbvrexcsf 2909 cbvreucsf 2910 cbvrabcsf 2911 csbprc 3262 un00 3263 disjssun 3285 disjpr2 3434 tppreq3 3473 diftpsn3 3505 preq12b 3541 intsng 3649 uniintsnr 3651 rint0 3654 riin0 3728 iununir 3738 intexr 3904 sucprc 4149 op1stbg 4210 elreldm 4560 xpeq0r 4746 xpdisj1 4747 xpdisj2 4748 resdisj 4751 xpima1 4767 xpima2m 4768 elxp4 4808 unixp0im 4854 uniabio 4877 iotass 4884 cnvresid 4973 funimacnv 4975 f1o00 5161 dffv4g 5175 fnrnfv 5220 feqresmpt 5227 dffn5imf 5228 funfvdm2f 5238 fvun1 5239 fvmpt2 5254 fndmin 5274 fmptcof 5331 fmptcos 5332 fvunsng 5357 fvpr1 5365 fnrnov 5646 offval 5719 ofrfval 5720 op1std 5775 op2ndd 5776 fmpt2co 5837 tpostpos 5879 rdgival 5969 frec0g 5983 2oconcl 6022 om0 6038 oei0 6039 oasuc 6044 omv2 6045 nnm0r 6058 uniqs2 6166 en1 6279 en1bg 6280 fundmen 6286 xpsnen 6295 xpcomco 6300 xpdom2 6305 nq0m0r 6554 addpinq1 6562 genipv 6607 genpelvl 6610 genpelvu 6611 cauappcvgprlem1 6757 caucvgsrlemoffres 6884 addresr 6913 mulresr 6914 axcnre 6955 add20 7469 rimul 7576 rereim 7577 mulreim 7595 div4p1lem1div2 8177 nnm1nn0 8223 znegcl 8276 peano2z 8281 nneoor 8340 nn0ind-raph 8355 xnegneg 8746 xltnegi 8748 fzo0to2pr 9074 fldiv4p1lem1div2 9147 frecfzennn 9203 exp0 9259 expp1 9262 expnegap0 9263 1exp 9284 mulexp 9294 sq0i 9345 bernneq 9369 imre 9451 reim0b 9462 rereb 9463 resqrexlemover 9608 resqrexlemcalc1 9612 abs00bd 9664 climconst 9811 ex-ceil 9896 bj-intexr 10028 |
Copyright terms: Public domain | W3C validator |