MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqeqan12d Structured version   Visualization version   Unicode version

Theorem eqeqan12d 2487
Description: A useful inference for substituting definitions into an equality. See also eqeqan12dALT 2488. (Contributed by NM, 9-Aug-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 20-Nov-2019.)
Hypotheses
Ref Expression
eqeqan12d.1  |-  ( ph  ->  A  =  B )
eqeqan12d.2  |-  ( ps 
->  C  =  D
)
Assertion
Ref Expression
eqeqan12d  |-  ( (
ph  /\  ps )  ->  ( A  =  C  <-> 
B  =  D ) )

Proof of Theorem eqeqan12d
StepHypRef Expression
1 eqeqan12d.1 . . 3  |-  ( ph  ->  A  =  B )
21adantr 472 . 2  |-  ( (
ph  /\  ps )  ->  A  =  B )
3 eqeqan12d.2 . . 3  |-  ( ps 
->  C  =  D
)
43adantl 473 . 2  |-  ( (
ph  /\  ps )  ->  C  =  D )
52, 4eqeq12d 2486 1  |-  ( (
ph  /\  ps )  ->  ( A  =  C  <-> 
B  =  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 376    = wceq 1452
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-an 378  df-cleq 2464
This theorem is referenced by:  eqeqan12rd  2489  eqfnfv2  5992  f1mpt  6180  soisores  6236  xpopth  6851  f1o2ndf1  6923  fnwelem  6930  fnse  6932  tz7.48lem  7176  ecopoveq  7482  xpdom2  7685  unfilem2  7854  wemaplem1  8079  suc11reg  8142  oemapval  8206  cantnf  8216  wemapwe  8220  r0weon  8461  infxpen  8463  fodomacn  8505  sornom  8725  fin1a2lem2  8849  fin1a2lem4  8851  neg11  9945  subeqrev  10063  rpnnen1  11318  cnref1o  11320  xneg11  11531  injresinj  12057  modadd1  12167  modmul1  12177  modlteq  12197  sq11  12385  hashen  12568  fz1eqb  12574  eqwrd  12759  s111  12806  wrd2ind  12888  wwlktovf1  13107  cj11  13302  sqrt11  13403  sqabs  13447  recan  13476  reeff1  14251  efieq  14294  eulerthlem2  14809  vdwlem12  15021  xpsff1o  15552  ismhm  16662  gsmsymgreq  17151  symgfixf1  17156  odf1  17291  sylow1  17333  frgpuplem  17500  isdomn  18595  cygznlem3  19217  psgnghm  19225  tgtop11  20075  fclsval  21101  vitali  22650  recosf1o  23563  dvdsmulf1o  24202  fsumvma  24220  brcgr  25009  axlowdimlem15  25065  axcontlem1  25073  axcontlem4  25076  axcontlem7  25079  axcontlem8  25080  iswlk  25327  istrl  25346  wlknwwlkninj  25518  wlkiswwlkinj  25525  wwlkextinj  25537  clwwlkf1  25603  numclwlk1lem2f1  25901  grpoinvf  26049  hial2eq2  26841  bnj554  29782  erdszelem9  29994  mrsubff1  30224  msubff1  30266  mvhf1  30269  nodenselem5  30645  fneval  31079  topfneec2  31083  f1omptsnlem  31808  f1omptsn  31809  rdgeqoa  31843  poimirlem4  32008  poimirlem26  32030  poimirlem27  32031  ismtyval  32196  wepwsolem  35971  fnwe2val  35978  aomclem8  35990  relexp0eq  36364  is1wlk  39815  isWlk  39816  ismgmhm  40291  2zlidl  40442
  Copyright terms: Public domain W3C validator