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

Theorem eqeqan12d 2453
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 2450 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  =  C  <-> 
B  =  D ) )
41, 2, 3syl2an 465 1  |-  ( (
ph  /\  ps )  ->  ( A  =  C  <-> 
B  =  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360    = wceq 1653
This theorem is referenced by:  eqeqan12rd  2454  eqfnfv2  5830  f1mpt  6009  soisores  6049  xpopth  6390  f1o2ndf1  6456  fnwelem  6463  fnse  6465  tz7.48lem  6700  ecopoveq  7007  xpdom2  7205  unfilem2  7374  wemaplem1  7517  suc11reg  7576  oemapval  7641  cantnf  7651  wemapwe  7656  r0weon  7896  infxpen  7898  fodomacn  7939  sornom  8159  fin1a2lem2  8283  fin1a2lem4  8285  addsrpr  8952  mulsrpr  8953  neg11  9354  rpnnen1  10607  cnref1o  10609  xneg11  10803  injresinj  11202  modadd1  11280  modmul1  11281  sq11  11456  hashen  11633  fz1eqb  11639  s111  11764  cj11  11969  sqr11  12070  sqabs  12114  recan  12142  reeff1  12723  efieq  12766  xpnnenOLD  12811  eulerthlem2  13173  vdwlem12  13362  xpsff1o  13795  ismhm  14742  odf1  15200  sylow1  15239  frgpuplem  15406  isdomn  16356  cygznlem3  16852  tgtop11  17049  fclsval  18042  vitali  19507  recosf1o  20439  dvdsmulf1o  20981  fsumvma  20999  iswlk  21529  istrl  21539  grpoinvf  21830  hial2eq2  22611  erdszelem9  24887  subeqrev  25199  nodenselem5  25642  brcgr  25841  axlowdimlem15  25897  axcontlem1  25905  axcontlem4  25908  axcontlem7  25911  axcontlem8  25912  fneval  26369  topfneec2  26374  ismtyval  26511  wepwsolem  27118  fnwe2val  27126  aomclem8  27138  psgnghm  27416  wrdeq0  28192  bnj554  29332
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-cleq 2431
  Copyright terms: Public domain W3C validator