![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eqtr4di | GIF version |
Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
eqtr4di.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
eqtr4di.2 | ⊢ 𝐶 = 𝐵 |
Ref | Expression |
---|---|
eqtr4di | ⊢ (𝜑 → 𝐴 = 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqtr4di.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | eqtr4di.2 | . . 3 ⊢ 𝐶 = 𝐵 | |
3 | 2 | eqcomi 2181 | . 2 ⊢ 𝐵 = 𝐶 |
4 | 1, 3 | eqtrdi 2226 | 1 ⊢ (𝜑 → 𝐴 = 𝐶) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1353 |
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: 3eqtr4g 2235 rabxmdc 3454 relop 4773 csbcnvg 4807 dfiun3g 4880 dfiin3g 4881 resima2 4937 relcnvfld 5158 uniabio 5184 fntpg 5268 dffn5im 5557 dfimafn2 5561 fncnvima2 5633 fmptcof 5679 fcoconst 5683 fnasrng 5692 ffnov 5973 fnovim 5977 fnrnov 6014 foov 6015 funimassov 6018 ovelimab 6019 ofc12 6097 caofinvl 6099 dftpos3 6257 tfr0dm 6317 rdgisucinc 6380 oasuc 6459 ecinxp 6604 phplem1 6846 exmidpw 6902 exmidpweq 6903 unfiin 6919 fidcenumlemr 6948 0ct 7100 ctmlemr 7101 exmidaclem 7201 indpi 7332 nqnq0pi 7428 nq0m0r 7446 addnqpr1 7552 recexgt0sr 7763 suplocsrlempr 7797 recidpipr 7846 recidpirq 7848 axrnegex 7869 nntopi 7884 cnref1o 9639 fztp 10064 fseq1m1p1 10081 fz0to4untppr 10110 frecuzrdgrrn 10394 frecuzrdgsuc 10400 frecuzrdgsuctlem 10409 seq3val 10444 seqvalcd 10445 fser0const 10502 mulexpzap 10546 expaddzap 10550 bcp1m1 10729 cjexp 10886 rexuz3 10983 bdtri 11232 climconst 11282 sumfct 11366 zsumdc 11376 fsum3 11379 sum0 11380 fsumcnv 11429 mertenslem2 11528 zproddc 11571 fprodseq 11575 prod0 11577 prod1dc 11578 prodfct 11579 fprodcnv 11617 ef0lem 11652 efzval 11675 efival 11724 sinbnd 11744 cosbnd 11745 eucalgval 12037 eucalginv 12039 eucalglt 12040 eucalgcvga 12041 eucalg 12042 sqpweven 12158 2sqpwodd 12159 dfphi2 12203 phimullem 12208 prmdiv 12218 odzval 12224 pcval 12279 pczpre 12280 pcrec 12291 ennnfonelemhdmp1 12393 ennnfonelemkh 12396 ressinbasd 12515 topnvalg 12648 ismgm 12668 plusffvalg 12673 grpidvalg 12684 issgrp 12701 ismnddef 12711 ismhm 12743 isgrp 12773 grpn0 12798 grpinvfvalg 12805 grpsubfvalg 12808 mulgfvalg 12874 mulgval 12875 mulgnn0p1 12883 iscmn 12923 mgpvalg 12960 issrg 12974 isring 13009 iscrng 13012 opprvalg 13066 istps 13197 cldval 13266 ntrfval 13267 clsfval 13268 neifval 13307 restbasg 13335 tgrest 13336 txval 13422 upxp 13439 uptx 13441 txrest 13443 lmcn2 13447 cnmpt2t 13460 cnmpt2res 13464 imasnopn 13466 psmetxrge0 13499 xmetge0 13532 isxms 13618 isms 13620 bdxmet 13668 qtopbasss 13688 cnblcld 13702 negfcncf 13756 dvfvalap 13817 eldvap 13818 dvidlemap 13827 dvexp2 13843 dvrecap 13844 dveflem 13854 sin0pilem1 13869 ptolemy 13912 coskpi 13936 logbrec 14045 lgslem1 14068 lgsval 14072 lgsval4 14088 lgsfcl3 14089 lgsdilem 14095 lgsdir2lem4 14099 lgsdir2lem5 14100 nninfsellemqall 14420 |
Copyright terms: Public domain | W3C validator |