![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > syl6eq | GIF 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 2114 | 1 ⊢ (𝜑 → 𝐴 = 𝐶) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1285 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-5 1377 ax-gen 1379 ax-4 1441 ax-17 1460 ax-ext 2064 |
This theorem depends on definitions: df-bi 115 df-cleq 2075 |
This theorem is referenced by: syl6req 2131 syl6eqr 2132 3eqtr3g 2137 3eqtr4a 2140 cbvralcsf 2965 cbvrexcsf 2966 cbvreucsf 2967 cbvrabcsf 2968 csbprc 3296 un00 3297 disjssun 3314 disjpr2 3464 tppreq3 3503 diftpsn3 3535 preq12b 3570 intsng 3678 uniintsnr 3680 rint0 3683 riin0 3757 iununir 3767 intexr 3933 sucprc 4175 op1stbg 4236 elreldm 4588 xpeq0r 4776 xpdisj1 4777 xpdisj2 4778 resdisj 4781 xpima1 4797 xpima2m 4798 elxp4 4838 unixp0im 4884 uniabio 4907 iotass 4914 cnvresid 5004 funimacnv 5006 f1o00 5192 dffv4g 5206 fnrnfv 5252 feqresmpt 5259 dffn5imf 5260 funfvdm2f 5270 fvun1 5271 fvmpt2 5286 fndmin 5306 fmptcof 5363 fmptcos 5364 fvunsng 5389 fvpr1 5397 fnrnov 5677 offval 5750 ofrfval 5751 op1std 5806 op2ndd 5807 fmpt2co 5868 tpostpos 5913 tfr0 5972 rdgival 6031 frec0g 6046 2oconcl 6086 om0 6102 oei0 6103 oasuc 6108 omv2 6109 nnm0r 6123 uniqs2 6232 en1 6346 en1bg 6347 fundmen 6353 xpsnen 6365 xpcomco 6370 xpdom2 6375 unsnfidcex 6440 en2other2 6522 nq0m0r 6708 addpinq1 6716 genipv 6761 genpelvl 6764 genpelvu 6765 cauappcvgprlem1 6911 caucvgsrlemoffres 7038 addresr 7067 mulresr 7068 axcnre 7109 add20 7645 rimul 7752 rereim 7753 mulreim 7771 div4p1lem1div2 8351 nnm1nn0 8396 znegcl 8463 peano2z 8468 nneoor 8530 nn0ind-raph 8545 xnegneg 8976 xltnegi 8978 fzo0to2pr 9304 fldiv4p1lem1div2 9387 mulp1mod1 9447 frecfzennn 9508 exp0 9577 expp1 9580 expnegap0 9581 1exp 9602 mulexp 9612 m1expeven 9620 sq0i 9664 bernneq 9690 facp1 9754 faclbnd3 9767 facubnd 9769 ibcval5 9787 sizeinf 9802 sizesng 9822 imre 9876 reim0b 9887 rereb 9888 resqrexlemover 10034 resqrexlemcalc1 10038 abs00bd 10090 maxabslemlub 10231 climconst 10267 dvdsabseq 10392 odd2np1lem 10416 oddp1even 10420 opoe 10439 m1expo 10444 m1exp1 10445 nn0o1gt2 10449 gcddvds 10499 gcdcl 10502 gcdeq0 10512 gcd0id 10514 bezoutr1 10566 eucialg 10585 lcm0val 10591 lcmid 10606 rpmul 10624 ex-ceil 10742 bj-intexr 10884 |
Copyright terms: Public domain | W3C validator |