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

Theorem eqeqan12d 2419
Description: A useful inference for substituting definitions into an equality. (Contributed by NM, 9-Aug-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)
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 . 2  |-  ( ph  ->  A  =  B )
2 eqeqan12d.2 . 2  |-  ( ps 
->  C  =  D
)
3 eqeq12 2416 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  =  C  <-> 
B  =  D ) )
41, 2, 3syl2an 464 1  |-  ( (
ph  /\  ps )  ->  ( A  =  C  <-> 
B  =  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1649
This theorem is referenced by:  eqeqan12rd  2420  eqfnfv2  5787  f1mpt  5966  soisores  6006  xpopth  6347  f1o2ndf1  6413  fnwelem  6420  fnse  6422  tz7.48lem  6657  ecopoveq  6964  xpdom2  7162  unfilem2  7331  wemaplem1  7471  suc11reg  7530  oemapval  7595  cantnf  7605  wemapwe  7610  r0weon  7850  infxpen  7852  fodomacn  7893  sornom  8113  fin1a2lem2  8237  fin1a2lem4  8239  addsrpr  8906  mulsrpr  8907  neg11  9308  rpnnen1  10561  cnref1o  10563  xneg11  10757  injresinj  11155  modadd1  11233  modmul1  11234  sq11  11409  hashen  11586  fz1eqb  11592  s111  11717  cj11  11922  sqr11  12023  sqabs  12067  recan  12095  reeff1  12676  efieq  12719  xpnnenOLD  12764  eulerthlem2  13126  vdwlem12  13315  xpsff1o  13748  ismhm  14695  odf1  15153  sylow1  15192  frgpuplem  15359  isdomn  16309  cygznlem3  16805  tgtop11  17002  fclsval  17993  vitali  19458  recosf1o  20390  dvdsmulf1o  20932  fsumvma  20950  iswlk  21480  istrl  21490  grpoinvf  21781  hial2eq2  22562  erdszelem9  24838  subeqrev  25150  nodenselem5  25553  brcgr  25743  axlowdimlem15  25799  axcontlem1  25807  axcontlem4  25810  axcontlem7  25813  axcontlem8  25814  fneval  26257  topfneec2  26262  ismtyval  26399  wepwsolem  27006  fnwe2val  27014  aomclem8  27027  psgnghm  27305  bnj554  28976
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-cleq 2397
  Copyright terms: Public domain W3C validator