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 2760. (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 2740 | . 2 ⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶)) |
3 | eqeqan12d.2 | . . 3 ⊢ (𝜓 → 𝐶 = 𝐷) | |
4 | 3 | eqeq2d 2749 | . 2 ⊢ (𝜓 → (𝐵 = 𝐶 ↔ 𝐵 = 𝐷)) |
5 | 2, 4 | sylan9bb 510 | 1 ⊢ ((𝜑 ∧ 𝜓) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1539 |
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 1913 ax-6 1971 ax-7 2011 ax-9 2116 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1783 df-cleq 2730 |
This theorem is referenced by: eqeqan12rd 2753 eqeq12d 2754 eqeq12 2755 eqfnfv2 6910 f1mpt 7134 soisores 7198 xpopth 7872 f1o2ndf1 7963 fnwelem 7972 fnse 7974 tz7.48lem 8272 ecopoveq 8607 xpdom2 8854 unfilem2 9079 wemaplem1 9305 suc11reg 9377 oemapval 9441 cantnf 9451 wemapwe 9455 r0weon 9768 infxpen 9770 fodomacn 9812 sornom 10033 fin1a2lem2 10157 fin1a2lem4 10159 neg11 11272 subeqrev 11397 rpnnen1lem6 12722 cnref1o 12725 xneg11 12949 injresinj 13508 modadd1 13628 modmul1 13644 modlteq 13665 sq11 13850 hashen 14061 fz1eqb 14069 eqwrd 14260 s111 14320 ccatopth 14429 wrd2ind 14436 wwlktovf1 14672 cj11 14873 sqrt11 14974 sqabs 15019 recan 15048 reeff1 15829 efieq 15872 eulerthlem2 16483 vdwlem12 16693 xpsff1o 17278 ismhm 18432 gsmsymgreq 19040 symgfixf1 19045 odf1 19169 sylow1 19208 frgpuplem 19378 isdomn 20565 cygznlem3 20777 psgnghm 20785 tgtop11 22132 fclsval 23159 vitali 24777 recosf1o 25691 dvdsmulf1o 26343 fsumvma 26361 brcgr 27268 axlowdimlem15 27324 axcontlem1 27332 axcontlem4 27335 axcontlem7 27338 axcontlem8 27339 iswlk 27977 wlkswwlksf1o 28244 wwlksnextinj 28264 clwlkclwwlkf1 28374 clwwlkf1 28413 numclwwlkqhash 28739 grpoinvf 28894 hial2eq2 29469 qusker 31549 bnj554 32879 erdszelem9 33161 sategoelfvb 33381 mrsubff1 33476 msubff1 33518 mvhf1 33521 fneval 34541 topfneec2 34545 bj-imdirval3 35355 f1omptsnlem 35507 f1omptsn 35508 rdgeqoa 35541 poimirlem4 35781 poimirlem26 35803 poimirlem27 35804 ismtyval 35958 extep 36418 brdmqss 36759 wepwsolem 40867 fnwe2val 40874 aomclem8 40886 relexp0eq 41309 sprsymrelf1 44948 fmtnof1 44987 fmtnofac1 45022 prmdvdsfmtnof1 45039 sfprmdvdsmersenne 45055 isupwlk 45298 uspgrsprf1 45309 ismgmhm 45337 2zlidl 45492 rrx2xpref1o 46064 rrx2plord 46066 rrx2plordisom 46069 sphere 46093 line2ylem 46097 |
Copyright terms: Public domain | W3C validator |