![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > eqeqan12d | Structured version Visualization version GIF version |
Description: A useful inference for substituting definitions into an equality. See also eqeqan12dALT 2759. (Contributed by NM, 9-Aug-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.) Shorten other proofs. (Revised by Wolf Lammen, 23-Oct-2024.) |
Ref | Expression |
---|---|
eqeqan12d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
eqeqan12d.2 | ⊢ (𝜓 → 𝐶 = 𝐷) |
Ref | Expression |
---|---|
eqeqan12d | ⊢ ((𝜑 ∧ 𝜓) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeqan12d.1 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | 1 | eqeq1d 2739 | . 2 ⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶)) |
3 | eqeqan12d.2 | . . 3 ⊢ (𝜓 → 𝐶 = 𝐷) | |
4 | 3 | eqeq2d 2748 | . 2 ⊢ (𝜓 → (𝐵 = 𝐶 ↔ 𝐵 = 𝐷)) |
5 | 2, 4 | sylan9bb 511 | 1 ⊢ ((𝜑 ∧ 𝜓) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 = wceq 1542 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-9 2117 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-cleq 2729 |
This theorem is referenced by: eqeqan12rd 2752 eqeq12d 2753 eqeq12 2754 eqfnfv2 6988 f1mpt 7213 soisores 7277 xpopth 7967 f1o2ndf1 8059 fnwelem 8068 fnse 8070 tz7.48lem 8392 ecopoveq 8764 xpdom2 9018 unfilem2 9262 wemaplem1 9489 suc11reg 9562 oemapval 9626 cantnf 9636 wemapwe 9640 r0weon 9955 infxpen 9957 fodomacn 9999 sornom 10220 fin1a2lem2 10344 fin1a2lem4 10346 neg11 11459 subeqrev 11584 rpnnen1lem6 12914 cnref1o 12917 xneg11 13141 injresinj 13700 modadd1 13820 modmul1 13836 modlteq 13857 sq11 14043 hashen 14254 fz1eqb 14261 eqwrd 14452 s111 14510 ccatopth 14611 wrd2ind 14618 wwlktovf1 14853 cj11 15054 sqrt11 15154 sqabs 15199 recan 15228 reeff1 16009 efieq 16052 eulerthlem2 16661 vdwlem12 16871 xpsff1o 17456 ismhm 18610 gsmsymgreq 19221 symgfixf1 19226 odf1 19351 sylow1 19392 frgpuplem 19561 isdomn 20780 cygznlem3 20992 psgnghm 21000 tgtop11 22348 fclsval 23375 vitali 24993 recosf1o 25907 dvdsmulf1o 26559 fsumvma 26577 negs11 27367 brcgr 27891 axlowdimlem15 27947 axcontlem1 27955 axcontlem4 27958 axcontlem7 27961 axcontlem8 27962 iswlk 28600 wlkswwlksf1o 28866 wwlksnextinj 28886 clwlkclwwlkf1 28996 clwwlkf1 29035 numclwwlkqhash 29361 grpoinvf 29516 hial2eq2 30091 qusker 32181 bnj554 33551 erdszelem9 33833 sategoelfvb 34053 mrsubff1 34148 msubff1 34190 mvhf1 34193 fneval 34853 topfneec2 34857 bj-imdirval3 35684 f1omptsnlem 35836 f1omptsn 35837 rdgeqoa 35870 poimirlem4 36111 poimirlem26 36133 poimirlem27 36134 ismtyval 36288 extep 36772 brdmqss 37137 wepwsolem 41398 fnwe2val 41405 aomclem8 41417 onsucf1o 41636 relexp0eq 42047 sprsymrelf1 45762 fmtnof1 45801 fmtnofac1 45836 prmdvdsfmtnof1 45853 sfprmdvdsmersenne 45869 isupwlk 46112 uspgrsprf1 46123 ismgmhm 46151 2zlidl 46306 rrx2xpref1o 46878 rrx2plord 46880 rrx2plordisom 46883 sphere 46907 line2ylem 46911 |
Copyright terms: Public domain | W3C validator |