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 2839. (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 481 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐵) |
3 | eqeqan12d.2 | . . 3 ⊢ (𝜓 → 𝐶 = 𝐷) | |
4 | 3 | adantl 482 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝐶 = 𝐷) |
5 | 2, 4 | eqeq12d 2837 | 1 ⊢ ((𝜑 ∧ 𝜓) → (𝐴 = 𝐶 ↔ 𝐵 = 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 = wceq 1528 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-9 2115 ax-ext 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-cleq 2814 |
This theorem is referenced by: eqeqan12rd 2840 eqfnfv2 6796 f1mpt 7010 soisores 7069 xpopth 7721 f1o2ndf1 7809 fnwelem 7816 fnse 7818 tz7.48lem 8068 ecopoveq 8388 xpdom2 8601 unfilem2 8772 wemaplem1 8999 suc11reg 9071 oemapval 9135 cantnf 9145 wemapwe 9149 r0weon 9427 infxpen 9429 fodomacn 9471 sornom 9688 fin1a2lem2 9812 fin1a2lem4 9814 neg11 10926 subeqrev 11051 rpnnen1lem6 12371 cnref1o 12374 xneg11 12598 injresinj 13148 modadd1 13266 modmul1 13282 modlteq 13303 sq11 13486 hashen 13697 fz1eqb 13705 eqwrd 13899 s111 13959 ccatopth 14068 wrd2ind 14075 wwlktovf1 14311 cj11 14511 sqrt11 14612 sqabs 14657 recan 14686 reeff1 15463 efieq 15506 eulerthlem2 16109 vdwlem12 16318 xpsff1o 16830 ismhm 17948 gsmsymgreq 18491 symgfixf1 18496 odf1 18620 sylow1 18659 frgpuplem 18829 isdomn 19997 cygznlem3 20646 psgnghm 20654 tgtop11 21520 fclsval 22546 vitali 24143 recosf1o 25046 dvdsmulf1o 25699 fsumvma 25717 brcgr 26614 axlowdimlem15 26670 axcontlem1 26678 axcontlem4 26681 axcontlem7 26684 axcontlem8 26685 iswlk 27320 wlkswwlksf1o 27585 wwlksnextinj 27605 clwlkclwwlkf1 27716 clwwlkf1 27756 numclwwlkqhash 28082 grpoinvf 28237 hial2eq2 28812 qusker 30846 bnj554 32071 erdszelem9 32344 sategoelfvb 32564 mrsubff1 32659 msubff1 32701 mvhf1 32704 fneval 33598 topfneec2 33602 bj-imdirval3 34367 f1omptsnlem 34500 f1omptsn 34501 rdgeqoa 34534 poimirlem4 34778 poimirlem26 34800 poimirlem27 34801 ismtyval 34961 extep 35423 brdmqss 35763 wepwsolem 39522 fnwe2val 39529 aomclem8 39541 relexp0eq 39926 sprsymrelf1 43505 fmtnof1 43544 fmtnofac1 43579 prmdvdsfmtnof1 43596 sfprmdvdsmersenne 43615 isupwlk 43858 uspgrsprf1 43869 ismgmhm 43897 2zlidl 44103 rrx2xpref1o 44603 rrx2plord 44605 rrx2plordisom 44608 sphere 44632 line2ylem 44636 |
Copyright terms: Public domain | W3C validator |