![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3eqtrd | GIF version |
Description: A deduction from three chained equalities. (Contributed by NM, 29-Oct-1995.) |
Ref | Expression |
---|---|
3eqtrd.1 | ⊢ (φ → A = B) |
3eqtrd.2 | ⊢ (φ → B = 𝐶) |
3eqtrd.3 | ⊢ (φ → 𝐶 = 𝐷) |
Ref | Expression |
---|---|
3eqtrd | ⊢ (φ → A = 𝐷) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3eqtrd.1 | . 2 ⊢ (φ → A = B) | |
2 | 3eqtrd.2 | . . 3 ⊢ (φ → B = 𝐶) | |
3 | 3eqtrd.3 | . . 3 ⊢ (φ → 𝐶 = 𝐷) | |
4 | 2, 3 | eqtrd 2069 | . 2 ⊢ (φ → B = 𝐷) |
5 | 1, 4 | 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: tpeq123d 3453 diftpsn3 3496 oteq123d 3555 resiima 4626 fvun1 5182 fvmptd 5196 fmptpr 5298 caovlem2d 5635 offval 5661 fnofval 5663 cnvf1olem 5787 nnm1 6033 ltexnqq 6391 prarloclemarch 6401 ltrnqg 6403 nq02m 6448 prarloclemcalc 6485 mulnqprl 6549 mulnqpru 6550 ltexprlemloc 6581 addcanprleml 6588 recexprlem1ssu 6606 cauappcvgprlem1 6631 axmulass 6757 axrnegex 6763 addcan2 6989 addsub 7019 subsub2 7035 negsubdi2 7066 muladd 7177 mulsub 7194 cru 7386 mulreim 7388 recextlem1 7414 mulap0 7417 muleqadd 7431 divrecap 7449 div23ap 7452 div12ap 7455 divcanap7 7479 conjmulap 7487 apmul1 7546 nndivtr 7736 qapne 8350 xnegneg 8516 fseq1p1m1 8726 nn0split 8764 fzosplitsnm1 8835 fzosplitprm1 8860 frecuzrdgsuc 8882 exp1 8915 expnegap0 8917 expmulzap 8955 expdivap 8959 binom3 9019 crim 9086 remullem 9099 remul2 9101 immul2 9108 ipcnval 9114 cjreim 9131 absid 9225 |
Copyright terms: Public domain | W3C validator |