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

Theorem eqeqan12d 2490
Description: A useful inference for substituting definitions into an equality. (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 465 . 2  |-  ( (
ph  /\  ps )  ->  A  =  B )
3 eqeqan12d.2 . . 3  |-  ( ps 
->  C  =  D
)
43adantl 466 . 2  |-  ( (
ph  /\  ps )  ->  C  =  D )
52, 4eqeq12d 2489 1  |-  ( (
ph  /\  ps )  ->  ( A  =  C  <-> 
B  =  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1379
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2459
This theorem is referenced by:  eqeqan12rd  2492  eqfnfv2  5983  f1mpt  6168  soisores  6222  xpopth  6834  f1o2ndf1  6903  fnwelem  6910  fnse  6912  tz7.48lem  7118  ecopoveq  7424  xpdom2  7624  unfilem2  7797  wemaplem1  7983  suc11reg  8048  oemapval  8114  cantnf  8124  cantnfOLD  8146  wemapwe  8151  wemapweOLD  8152  r0weon  8402  infxpen  8404  fodomacn  8449  sornom  8669  fin1a2lem2  8793  fin1a2lem4  8795  neg11  9882  subeqrev  9994  rpnnen1  11225  cnref1o  11227  xneg11  11426  injresinj  11906  modadd1  12013  modmul1  12020  sq11  12220  hashen  12400  fz1eqb  12406  eqwrd  12562  s111  12603  wrd2ind  12683  wwlktovf1  12875  cj11  12975  sqrt11  13076  sqabs  13120  recan  13149  reeff1  13733  efieq  13776  xpnnenOLD  13821  eulerthlem2  14188  vdwlem12  14386  xpsff1o  14840  ismhm  15841  gsmsymgreq  16329  symgfixf1  16335  odf1  16457  sylow1  16496  frgpuplem  16663  isdomn  17813  cygznlem3  18477  psgnghm  18485  tgtop11  19352  fclsval  20377  vitali  21890  recosf1o  22788  dvdsmulf1o  23336  fsumvma  23354  brcgr  24017  axlowdimlem15  24073  axcontlem1  24081  axcontlem4  24084  axcontlem7  24087  axcontlem8  24088  iswlk  24334  istrl  24353  wlknwwlkninj  24525  wlkiswwlkinj  24532  wwlkextinj  24544  clwwlkf1  24610  numclwlk1lem2f1  24909  grpoinvf  25056  hial2eq2  25838  erdszelem9  28459  mrsubff1  28690  msubff1  28732  mvhf1  28735  nodenselem5  29363  fneval  30088  topfneec2  30092  ismtyval  30214  wepwsolem  30906  fnwe2val  30914  aomclem8  30926  bnj554  33392
  Copyright terms: Public domain W3C validator