| 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 2743 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) |
| 3 | sylan9req.2 | . 2 ⊢ (𝜓 → 𝐵 = 𝐶) | |
| 4 | 2, 3 | sylan9eq 2797 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-cleq 2729 |
| This theorem is referenced by: ordintdif 6434 fndmu 6675 fodmrnu 6828 funcoeqres 6879 eqfnun 7057 sspreima 7088 tz7.44-3 8448 fsetfocdm 8901 dfac5lem4 10166 dfac5lem4OLD 10168 zdiv 12688 hashimarni 14480 fprodss 15984 dvdsmulc 16321 smumullem 16529 cncongrcoprm 16707 mgmidmo 18673 reslmhm2b 21053 fclsfnflim 24035 ustuqtop1 24250 ulm2 26428 sineq0 26566 cxple2a 26741 sqff1o 27225 lgsmodeq 27386 eedimeq 28913 frrusgrord0 30359 grpoidinvlem4 30526 hlimuni 31257 dmdsl3 32334 atoml2i 32402 disjpreima 32597 xrge0npcan 33025 poimirlem3 37630 poimirlem4 37631 poimirlem16 37643 poimirlem17 37644 poimirlem19 37646 poimirlem20 37647 poimirlem23 37650 poimirlem24 37651 poimirlem25 37652 poimirlem29 37656 poimirlem31 37658 unidmqs 38655 ltrncnvnid 40129 cdleme20j 40320 cdleme42ke 40487 dia2dimlem13 41078 dvh4dimN 41449 mapdval4N 41634 ccatcan2d 42292 zdivgd 42372 cnreeu 42500 sineq0ALT 44957 cncfiooicc 45909 fourierdlem41 46163 fourierdlem71 46192 bgoldbtbndlem4 47795 bgoldbtbnd 47796 isubgr3stgrlem8 47940 |
| Copyright terms: Public domain | W3C validator |