ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eqeq12d Unicode version

Theorem eqeq12d 2070
Description: A useful inference for substituting definitions into an equality. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
eqeq12d.1  |-  ( ph  ->  A  =  B )
eqeq12d.2  |-  ( ph  ->  C  =  D )
Assertion
Ref Expression
eqeq12d  |-  ( ph  ->  ( A  =  C  <-> 
B  =  D ) )

Proof of Theorem eqeq12d
StepHypRef Expression
1 eqeq12d.1 . 2  |-  ( ph  ->  A  =  B )
2 eqeq12d.2 . 2  |-  ( ph  ->  C  =  D )
3 eqeq12 2068 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  =  C  <-> 
B  =  D ) )
41, 2, 3syl2anc 397 1  |-  ( ph  ->  ( A  =  C  <-> 
B  =  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 102    = wceq 1259
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-4 1416  ax-17 1435  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-cleq 2049
This theorem is referenced by:  cdeqeq  2782  sbceqg  2894  csbing  3172  uniprg  3623  unisng  3625  intprg  3676  iununir  3766  csbopabg  3863  limeq  4142  onsucuni2  4316  ordpwsucexmid  4322  csbima12g  4714  dmsnsnsng  4826  cnvsng  4834  csbiotag  4923  fvmptf  5291  eqfnfv2f  5297  fvreseq  5299  fmptco  5358  fnressn  5377  fvsng  5387  cocan1  5455  cocan2  5456  fliftfun  5464  csbriotag  5508  csbov123g  5571  eqfnov  5635  ovmpt2s  5652  ov2gf  5653  ovmpt2dxf  5654  caovcomg  5684  caovassg  5687  caovcang  5690  caovcanrd  5692  caovcan  5693  caovdig  5703  caovdirg  5706  caovimo  5722  grprinvlem  5723  grprinvd  5724  offveqb  5758  op1stg  5805  op2ndg  5806  f1o2ndf1  5877  tfrlem1  5954  tfrlem3ag  5955  tfrlem3a  5956  tfrlem5  5961  tfrlem9  5966  tfr0  5968  tfrlemiubacc  5975  tfrlemiex  5976  tfrlemi1  5977  tfri3  5984  rdg0g  6006  frecrdg  6023  nna0r  6088  nnacom  6094  nnaass  6095  nndi  6096  nnmass  6097  nnmsucr  6098  nnmcom  6099  ecopovtrn  6234  ecopovsymg  6236  ecopovtrng  6237  ecovcom  6244  ecovicom  6245  ecovass  6246  ecoviass  6247  ecovdi  6248  ecovidi  6249  dom2lem  6283  ordiso2  6415  addcanpig  6490  mulcanpig  6491  mulcmpblnq  6524  mulpipqqs  6529  ordpipqqs  6530  mulidnq  6545  enq0sym  6588  nqnq0  6597  mulcmpblnq0  6600  distrnq0  6615  mulcomnq0  6616  addassnq0  6618  nq02m  6621  genipv  6665  cauappcvgprlemladd  6814  addcmpblnr  6882  0idsr  6910  1idsr  6911  axaddcom  7002  ax1rid  7009  ax0id  7010  rereceu  7021  axcaucvg  7032  mulid1  7082  readdcan  7214  cnegexlem1  7249  cnegexlem3  7251  addcan  7254  addcan2  7255  apti  7687  mulcanapd  7716  mulcanap2d  7717  div11ap  7751  divmuleqap  7768  conjmulap  7780  eqneg  7783  cnref1o  8680  fzsuc2  9043  fzprval  9046  fztpval  9047  qtri3or  9200  modqadd1  9311  modqmul1  9327  addmodlteq  9348  frec2uzrdg  9359  iseqss  9390  iseqfveq2  9392  iseqfveq  9394  iseqfeq  9395  iseqshft2  9396  iseqsplit  9402  iseqcaopr3  9404  iseqcaopr2  9405  iseqid  9411  iseqhomo  9412  mulexp  9459  expadd  9462  expmul  9465  nn0opth2d  9591  bcpasc  9634  shftvalg  9665  shftval4g  9666  replim  9687  cjreb  9694  cjexp  9721  absexp  9906  recan  9936  moddvds  10117  ialginv  10269  ialgfx  10274
  Copyright terms: Public domain W3C validator