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

Theorem eqeqan12d 2443
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 466 . 2  |-  ( (
ph  /\  ps )  ->  A  =  B )
3 eqeqan12d.2 . . 3  |-  ( ps 
->  C  =  D
)
43adantl 467 . 2  |-  ( (
ph  /\  ps )  ->  C  =  D )
52, 4eqeq12d 2442 1  |-  ( (
ph  /\  ps )  ->  ( A  =  C  <-> 
B  =  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370    = wceq 1437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-ext 2398
This theorem depends on definitions:  df-bi 188  df-an 372  df-cleq 2412
This theorem is referenced by:  eqeqan12rd  2445  eqfnfv2  5983  f1mpt  6168  soisores  6224  xpopth  6837  f1o2ndf1  6906  fnwelem  6913  fnse  6915  tz7.48lem  7157  ecopoveq  7463  xpdom2  7664  unfilem2  7833  wemaplem1  8052  suc11reg  8115  oemapval  8178  cantnf  8188  wemapwe  8192  r0weon  8433  infxpen  8435  fodomacn  8476  sornom  8696  fin1a2lem2  8820  fin1a2lem4  8822  neg11  9914  subeqrev  10031  rpnnen1  11284  cnref1o  11286  xneg11  11497  injresinj  12011  modadd1  12120  modmul1  12129  sq11  12333  hashen  12516  fz1eqb  12522  eqwrd  12684  s111  12726  wrd2ind  12808  wwlktovf1  13000  cj11  13193  sqrt11  13294  sqabs  13338  recan  13367  reeff1  14141  efieq  14184  eulerthlem2  14688  vdwlem12  14894  xpsff1o  15418  ismhm  16528  gsmsymgreq  17017  symgfixf1  17022  odf1  17144  sylow1  17183  frgpuplem  17350  isdomn  18446  cygznlem3  19064  psgnghm  19072  tgtop11  19922  fclsval  20947  vitali  22445  recosf1o  23346  dvdsmulf1o  23983  fsumvma  24001  brcgr  24773  axlowdimlem15  24829  axcontlem1  24837  axcontlem4  24840  axcontlem7  24843  axcontlem8  24844  iswlk  25090  istrl  25109  wlknwwlkninj  25281  wlkiswwlkinj  25288  wwlkextinj  25300  clwwlkf1  25366  numclwlk1lem2f1  25664  grpoinvf  25810  hial2eq2  26592  bnj554  29495  erdszelem9  29707  mrsubff1  29937  msubff1  29979  mvhf1  29982  nodenselem5  30356  fneval  30790  topfneec2  30794  f1omptsnlem  31469  f1omptsn  31470  poimirlem4  31648  poimirlem26  31670  poimirlem27  31671  ismtyval  31836  wepwsolem  35610  fnwe2val  35617  aomclem8  35629  relexp0eq  35936  ismgmhm  38554  2zlidl  38705
  Copyright terms: Public domain W3C validator