![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eqtr4d | GIF version |
Description: An equality transitivity equality deduction. (Contributed by NM, 18-Jul-1995.) |
Ref | Expression |
---|---|
eqtr4d.1 | ⊢ (φ → A = B) |
eqtr4d.2 | ⊢ (φ → 𝐶 = B) |
Ref | Expression |
---|---|
eqtr4d | ⊢ (φ → A = 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqtr4d.1 | . 2 ⊢ (φ → A = B) | |
2 | eqtr4d.2 | . . 3 ⊢ (φ → 𝐶 = B) | |
3 | 2 | eqcomd 2042 | . 2 ⊢ (φ → B = 𝐶) |
4 | 1, 3 | eqtrd 2069 | 1 ⊢ (φ → A = 𝐶) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1242 |
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: 3eqtr2d 2075 3eqtr2rd 2076 3eqtr4d 2079 3eqtr4rd 2080 3eqtr4a 2095 sbnfc2 2900 relop 4429 riinint 4536 iotauni 4822 fniinfv 5174 fsn2 5280 fmptapd 5297 fconst2g 5319 fniunfv 5344 ofres 5667 ofco 5671 frecsuclem2 5928 frecrdg 5931 oasuc 5983 nnacom 6002 nnaass 6003 nndi 6004 nnmass 6005 nnmsucr 6006 nnmcom 6007 uniqs2 6102 en1bg 6216 fundmen 6222 addcmpblnq 6351 distrnqg 6371 ltexnqq 6391 addcmpblnq0 6426 nqnq0a 6437 nqnq0m 6438 nq0m0r 6439 nq0a0 6440 nnanq0 6441 distrnq0 6442 prarloclemlo 6477 prarloclemcalc 6485 genpassl 6507 genpassu 6508 ltsosr 6692 0idsr 6695 1idsr 6696 mulextsr1lem 6706 cnegex 6986 subsub3 7039 subadd4 7051 mulneg12 7190 mulsub 7194 apreap 7371 cru 7386 recextlem1 7414 cju 7694 halfaddsub 7936 nn0supp 8010 nneo 8117 zeo2 8120 uzin 8281 iccf1o 8642 fzsuc2 8711 frec2uzrdg 8876 iseqfveq2 8905 expp1 8916 mulexp 8948 mulexpzap 8949 expadd 8951 expaddzap 8953 expmul 8954 expmulzap 8955 expsubap 8956 expdivap 8959 subsq 9011 binom3 9019 bernneq 9022 crre 9085 remim 9088 remullem 9099 cjexp 9121 cnrecnv 9138 abscj 9220 absid 9225 absre 9228 |
Copyright terms: Public domain | W3C validator |