![]() |
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 2668. (Contributed by NM, 9-Aug-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 20-Nov-2019.) |
Ref | Expression |
---|---|
eqeqan12d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
eqeqan12d.2 | ⊢ (𝜓 → 𝐶 = 𝐷) |
Ref | Expression |
---|---|
eqeqan12d | ⊢ ((𝜑 ∧ 𝜓) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeqan12d.1 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | 1 | adantr 480 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐵) |
3 | eqeqan12d.2 | . . 3 ⊢ (𝜓 → 𝐶 = 𝐷) | |
4 | 3 | adantl 481 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝐶 = 𝐷) |
5 | 2, 4 | eqeq12d 2666 | 1 ⊢ ((𝜑 ∧ 𝜓) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 383 = wceq 1523 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-an 385 df-ex 1745 df-cleq 2644 |
This theorem is referenced by: eqeqan12rd 2669 eqfnfv2 6352 f1mpt 6558 soisores 6617 xpopth 7251 f1o2ndf1 7330 fnwelem 7337 fnse 7339 tz7.48lem 7581 ecopoveq 7891 xpdom2 8096 unfilem2 8266 wemaplem1 8492 suc11reg 8554 oemapval 8618 cantnf 8628 wemapwe 8632 r0weon 8873 infxpen 8875 fodomacn 8917 sornom 9137 fin1a2lem2 9261 fin1a2lem4 9263 neg11 10370 subeqrev 10491 rpnnen1lem6 11857 rpnnen1OLD 11863 cnref1o 11865 xneg11 12084 injresinj 12629 modadd1 12747 modmul1 12763 modlteq 12784 sq11 12976 hashen 13175 fz1eqb 13183 eqwrd 13379 s111 13432 wrd2ind 13523 wwlktovf1 13746 cj11 13946 sqrt11 14047 sqabs 14091 recan 14120 reeff1 14894 efieq 14937 eulerthlem2 15534 vdwlem12 15743 xpsff1o 16275 ismhm 17384 gsmsymgreq 17898 symgfixf1 17903 odf1 18025 sylow1 18064 frgpuplem 18231 isdomn 19342 cygznlem3 19966 psgnghm 19974 tgtop11 20834 fclsval 21859 vitali 23427 recosf1o 24326 dvdsmulf1o 24965 fsumvma 24983 brcgr 25825 axlowdimlem15 25881 axcontlem1 25889 axcontlem4 25892 axcontlem7 25895 axcontlem8 25896 iswlk 26562 wlkpwwlkf1ouspgr 26833 wlknwwlksninj 26843 wlkwwlkinj 26850 wwlksnextinj 26862 clwwlkf1 27012 numclwwlkqhash 27355 grpoinvf 27514 hial2eq2 28092 bnj554 31095 erdszelem9 31307 mrsubff1 31537 msubff1 31579 mvhf1 31582 fneval 32472 topfneec2 32476 f1omptsnlem 33313 f1omptsn 33314 rdgeqoa 33348 poimirlem4 33543 poimirlem26 33565 poimirlem27 33566 ismtyval 33729 extep 34189 wepwsolem 37929 fnwe2val 37936 aomclem8 37948 relexp0eq 38310 fmtnof1 41772 fmtnofac1 41807 prmdvdsfmtnof1 41824 sfprmdvdsmersenne 41845 isupwlk 42042 sprsymrelf1 42071 uspgrsprf1 42080 ismgmhm 42108 2zlidl 42259 |
Copyright terms: Public domain | W3C validator |