![]() |
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 2069 |
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 1333 ax-gen 1335 ax-4 1397 ax-17 1416 ax-ext 2019 |
This theorem depends on definitions: df-bi 110 df-cleq 2030 |
This theorem is referenced by: syl6req 2086 syl6eqr 2087 3eqtr3g 2092 3eqtr4a 2095 cbvralcsf 2902 cbvrexcsf 2903 cbvreucsf 2904 cbvrabcsf 2905 csbprc 3256 un00 3257 disjssun 3279 disjpr2 3425 tppreq3 3464 diftpsn3 3496 preq12b 3532 intsng 3640 uniintsnr 3642 rint0 3645 riin0 3719 iununir 3729 intexr 3895 sucprc 4115 op1stbg 4176 elreldm 4503 xpeq0r 4689 xpdisj1 4690 xpdisj2 4691 resdisj 4694 xpima1 4710 xpima2m 4711 elxp4 4751 unixp0im 4797 uniabio 4820 iotass 4827 cnvresid 4916 funimacnv 4918 f1o00 5104 dffv4g 5118 fnrnfv 5163 feqresmpt 5170 dffn5imf 5171 funfvdm2f 5181 fvun1 5182 fvmpt2 5197 fndmin 5217 fmptcof 5274 fmptcos 5275 fvunsng 5300 fvpr1 5308 fnrnov 5588 offval 5661 ofrfval 5662 op1std 5717 op2ndd 5718 fmpt2co 5779 tpostpos 5820 rdgival 5909 frec0g 5922 2oconcl 5961 om0 5977 oei0 5978 oasuc 5983 omv2 5984 nnm0r 5997 uniqs2 6102 en1 6215 en1bg 6216 fundmen 6222 xpsnen 6231 xpcomco 6236 xpdom2 6241 nq0m0r 6439 addpinq1 6447 genipv 6492 genpelvl 6495 genpelvu 6496 cauappcvgprlem1 6631 addresr 6734 mulresr 6735 axcnre 6765 add20 7264 rimul 7369 rereim 7370 mulreim 7388 nnm1nn0 7999 znegcl 8052 peano2z 8057 nneoor 8116 nn0ind-raph 8131 xnegneg 8516 xltnegi 8518 fzo0to2pr 8844 frecfzennn 8884 exp0 8913 expp1 8916 expnegap0 8917 1exp 8938 mulexp 8948 sq0i 8998 bernneq 9022 imre 9079 reim0b 9090 rereb 9091 abs00bd 9224 bj-intexr 9363 |
Copyright terms: Public domain | W3C validator |