Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > eqtr4id | GIF version |
Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.) |
Ref | Expression |
---|---|
eqtr4id.2 | ⊢ 𝐴 = 𝐵 |
eqtr4id.1 | ⊢ (𝜑 → 𝐶 = 𝐵) |
Ref | Expression |
---|---|
eqtr4id | ⊢ (𝜑 → 𝐴 = 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqtr4id.1 | . 2 ⊢ (𝜑 → 𝐶 = 𝐵) | |
2 | eqtr4id.2 | . . 3 ⊢ 𝐴 = 𝐵 | |
3 | 2 | eqcomi 2168 | . 2 ⊢ 𝐵 = 𝐴 |
4 | 1, 3 | eqtr2di 2214 | 1 ⊢ (𝜑 → 𝐴 = 𝐶) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1342 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1434 ax-gen 1436 ax-4 1497 ax-17 1513 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-cleq 2157 |
This theorem is referenced by: iftrue 3520 iffalse 3523 difprsn1 3706 dmmptg 5095 relcoi1 5129 funimacnv 5258 dmmptd 5312 dffv3g 5476 dfimafn 5529 fvco2 5549 isoini 5780 oprabco 6176 ixpconstg 6664 unfiexmid 6874 undifdc 6880 sbthlemi4 6916 sbthlemi5 6917 sbthlemi6 6918 supval2ti 6951 exmidfodomrlemim 7148 suplocexprlemex 7654 eqneg 8619 zeo 9287 fseq1p1m1 10019 seq3val 10383 seqvalcd 10384 hashfzo 10724 hashxp 10728 fsumconst 11381 modfsummod 11385 telfsumo 11393 fprodconst 11547 mulgcd 11934 algcvg 11959 phiprmpw 12133 phisum 12151 strslfv3 12382 uptx 12821 resubmet 13095 |
Copyright terms: Public domain | W3C validator |