![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sylan9req | Structured version Visualization version GIF version |
Description: An equality transitivity deduction. (Contributed by NM, 23-Jun-2007.) |
Ref | Expression |
---|---|
sylan9req.1 | ⊢ (𝜑 → 𝐵 = 𝐴) |
sylan9req.2 | ⊢ (𝜓 → 𝐵 = 𝐶) |
Ref | Expression |
---|---|
sylan9req | ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylan9req.1 | . . 3 ⊢ (𝜑 → 𝐵 = 𝐴) | |
2 | 1 | eqcomd 2766 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) |
3 | sylan9req.2 | . 2 ⊢ (𝜓 → 𝐵 = 𝐶) | |
4 | 2, 3 | sylan9eq 2814 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 = wceq 1632 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-9 2148 ax-ext 2740 |
This theorem depends on definitions: df-bi 197 df-an 385 df-ex 1854 df-cleq 2753 |
This theorem is referenced by: ordintdif 5935 fndmu 6153 fodmrnu 6284 funcoeqres 6328 tz7.44-3 7673 dfac5lem4 9139 zdiv 11639 hashimarni 13420 ccatws1lenrevOLD 13606 fprodss 14877 dvdsmulc 15211 smumullem 15416 cncongrcoprm 15586 mgmidmo 17460 reslmhm2b 19256 fclsfnflim 22032 ustuqtop1 22246 ulm2 24338 sineq0 24472 cxple2a 24644 sqff1o 25107 lgsmodeq 25266 eedimeq 25977 frrusgrord0 27494 grpoidinvlem4 27670 hlimuni 28404 dmdsl3 29483 atoml2i 29551 disjpreima 29704 sspreima 29756 xrge0npcan 30003 poimirlem3 33725 poimirlem4 33726 poimirlem16 33738 poimirlem17 33739 poimirlem19 33741 poimirlem20 33742 poimirlem23 33745 poimirlem24 33746 poimirlem25 33747 poimirlem29 33751 poimirlem31 33753 eqfnun 33829 ltrncnvnid 35916 cdleme20j 36108 cdleme42ke 36275 dia2dimlem13 36867 dvh4dimN 37238 mapdval4N 37423 sineq0ALT 39672 cncfiooicc 40610 fourierdlem41 40868 fourierdlem71 40897 bgoldbtbndlem4 42206 bgoldbtbnd 42207 |
Copyright terms: Public domain | W3C validator |