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

Theorem eqeqan12d 2477
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 2476 1  |-  ( (
ph  /\  ps )  ->  ( A  =  C  <-> 
B  =  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1370
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2446
This theorem is referenced by:  eqeqan12rd  2479  eqfnfv2  5906  f1mpt  6082  soisores  6126  xpopth  6724  f1o2ndf1  6789  fnwelem  6796  fnse  6798  tz7.48lem  7005  ecopoveq  7310  xpdom2  7515  unfilem2  7687  wemaplem1  7870  suc11reg  7935  oemapval  8001  cantnf  8011  cantnfOLD  8033  wemapwe  8038  wemapweOLD  8039  r0weon  8289  infxpen  8291  fodomacn  8336  sornom  8556  fin1a2lem2  8680  fin1a2lem4  8682  addsrpr  9352  mulsrpr  9353  neg11  9770  subeqrev  9881  rpnnen1  11094  cnref1o  11096  xneg11  11295  injresinj  11755  modadd1  11861  modmul1  11868  sq11  12054  hashen  12234  fz1eqb  12240  eqwrd  12382  s111  12419  wrd2ind  12489  cj11  12768  sqr11  12869  sqabs  12913  recan  12941  reeff1  13521  efieq  13564  xpnnenOLD  13609  eulerthlem2  13974  vdwlem12  14170  xpsff1o  14624  ismhm  15584  gsmsymgreq  16055  symgfixf1  16061  odf1  16183  sylow1  16222  frgpuplem  16389  isdomn  17488  cygznlem3  18126  psgnghm  18134  tgtop11  18718  fclsval  19712  vitali  21225  recosf1o  22123  dvdsmulf1o  22666  fsumvma  22684  brcgr  23297  axlowdimlem15  23353  axcontlem1  23361  axcontlem4  23364  axcontlem7  23367  axcontlem8  23368  iswlk  23577  istrl  23587  grpoinvf  23878  hial2eq2  24660  erdszelem9  27230  nodenselem5  27969  fneval  28706  topfneec2  28711  ismtyval  28846  wepwsolem  29541  fnwe2val  29549  aomclem8  29561  wwlktovf1  30399  wlknwwlkninj  30490  wlkiswwlkinj  30497  wwlkextinj  30509  clwwlkf1  30605  numclwlk1lem2f1  30834  bnj554  32209
  Copyright terms: Public domain W3C validator