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 2616 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) |
3 | sylan9req.2 | . 2 ⊢ (𝜓 → 𝐵 = 𝐶) | |
4 | 2, 3 | sylan9eq 2664 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 = wceq 1475 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-an 385 df-cleq 2603 |
This theorem is referenced by: ordintdif 5691 fndmu 5906 fodmrnu 6036 funcoeqres 6080 tz7.44-3 7391 dfac5lem4 8832 zdiv 11323 hashimarni 13086 ccatws1lenrev 13260 fprodss 14517 dvdsmulc 14847 smumullem 15052 cncongrcoprm 15222 mgmidmo 17082 reslmhm2b 18875 fclsfnflim 21641 ustuqtop1 21855 ulm2 23943 sineq0 24077 cxple2a 24245 sqff1o 24708 lgsmodeq 24867 eedimeq 25578 grpoidinvlem4 26745 hlimuni 27479 dmdsl3 28558 atoml2i 28626 disjpreima 28779 sspreima 28827 xrge0npcan 29025 poimirlem3 32582 poimirlem4 32583 poimirlem16 32595 poimirlem17 32596 poimirlem19 32598 poimirlem20 32599 poimirlem23 32602 poimirlem24 32603 poimirlem25 32604 poimirlem29 32608 poimirlem31 32610 eqfnun 32686 ltrncnvnid 34431 cdleme20j 34624 cdleme42ke 34791 dia2dimlem13 35383 dvh4dimN 35754 mapdval4N 35939 sineq0ALT 38195 cncfiooicc 38780 fourierdlem41 39041 fourierdlem71 39070 bgoldbtbndlem4 40224 bgoldbtbnd 40225 |
Copyright terms: Public domain | W3C validator |