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

Theorem eqeq12d 2192
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 2190 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A  =  C  <-> 
B  =  D ) )
41, 2, 3syl2anc 411 1  |-  ( ph  ->  ( A  =  C  <-> 
B  =  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 105    = wceq 1353
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-cleq 2170
This theorem is referenced by:  cdeqeq  2957  sbceqg  3073  csbing  3342  uniprg  3822  unisng  3824  intprg  3875  iununir  3967  csbopabg  4078  undifexmid  4190  exmidundif  4203  exmidundifim  4204  limeq  4374  onsucuni2  4560  ordpwsucexmid  4566  csbima12g  4985  dmsnsnsng  5102  cnvsng  5110  csbiotag  5205  fvmptf  5604  eqfnfv2f  5613  fvreseq  5615  fmptco  5678  fnressn  5698  fvsng  5708  cocan1  5782  cocan2  5783  fliftfun  5791  csbriotag  5837  oveqrspc2v  5896  csbov123g  5907  eqfnov  5975  ovmpos  5992  ov2gf  5993  ovmpodxf  5994  caovcomg  6024  caovassg  6027  caovcang  6030  caovcanrd  6032  caovcan  6033  caovdig  6043  caovdirg  6046  caovimo  6062  offveqb  6096  op1stg  6145  op2ndg  6146  f1o2ndf1  6223  tfrlem1  6303  tfrlem3ag  6304  tfrlem3a  6305  tfrlem5  6309  tfrlem9  6314  tfr0dm  6317  tfrlemiubacc  6325  tfrlemiex  6326  tfrlemi1  6327  tfr1onlem3ag  6332  tfr1onlemubacc  6341  tfr1onlemex  6342  tfr1onlemaccex  6343  tfrcllemsucaccv  6349  tfrcllembxssdm  6351  tfrcllemubacc  6354  tfrcllemex  6355  tfrcllemaccex  6356  tfrcllemres  6357  tfrcldm  6358  tfri3  6362  rdg0g  6383  frecrdg  6403  nna0r  6473  nnacom  6479  nnaass  6480  nndi  6481  nnmass  6482  nnmsucr  6483  nnmcom  6484  ecopovtrn  6626  ecopovsymg  6628  ecopovtrng  6629  ecovcom  6636  ecovicom  6637  ecovass  6638  ecoviass  6639  ecovdi  6640  ecovidi  6641  dom2lem  6766  ordiso2  7028  inl11  7058  updjud  7075  omp1eomlem  7087  difinfsnlem  7092  nnnninfeq  7120  nninfwlporlemd  7164  nninfwlpor  7166  exmidfodomrlemrALT  7196  exmidaclem  7201  addcanpig  7321  mulcanpig  7322  mulcmpblnq  7355  mulpipqqs  7360  ordpipqqs  7361  mulidnq  7376  enq0sym  7419  nqnq0  7428  mulcmpblnq0  7431  distrnq0  7446  mulcomnq0  7447  addassnq0  7449  nq02m  7452  genipv  7496  cauappcvgprlemladd  7645  addcmpblnr  7726  0idsr  7754  1idsr  7755  axaddcom  7857  ax1rid  7864  ax0id  7865  rereceu  7876  axcaucvg  7887  mulid1  7942  readdcan  8084  cnegexlem1  8119  cnegexlem3  8121  addcan  8124  addcan2  8125  apti  8566  mulcanapd  8604  mulcanap2d  8605  div11ap  8643  divmuleqap  8660  conjmulap  8672  eqneg  8675  cnref1o  9636  fzsuc2  10062  fzprval  10065  fztpval  10066  qtri3or  10226  modqadd1  10344  modqmul1  10360  addmodlteq  10381  frec2uzrdg  10392  frecuzrdgg  10399  seq3val  10441  seqvalcd  10442  seq3fveq2  10452  seq3fveq  10454  seq3feq  10455  seq3shft2  10456  seq3split  10462  seq3caopr3  10464  seq3caopr2  10465  iseqf1olemkle  10467  iseqf1olemklt  10468  iseqf1olemqk  10477  seq3f1olemqsum  10483  seq3f1olemstep  10484  seq3f1olemp  10485  seq3f1oleml  10486  seq3id  10491  seq3id2  10492  seq3homo  10493  mulexp  10542  expadd  10545  expmul  10548  modqexp  10629  nn0opth2d  10684  bcpasc  10727  hashennn  10741  hashen  10745  omgadd  10763  hashfzo  10783  hashfzp1  10785  hashxp  10787  hashfacen  10797  seq3coll  10803  shftvalg  10826  shftval4g  10827  replim  10849  cjreb  10856  cjexp  10883  absexp  11069  recan  11099  minclpr  11226  mingeb  11231  sumeq2  11348  zsumdc  11373  fsum3  11376  fsumf1o  11379  fsum3cvg2  11383  fsumadd  11395  isummulc2  11415  fsum2d  11424  fsummulc2  11437  fsumconst  11443  modfsummod  11447  fsumparts  11459  fsumrelem  11460  fsumiun  11466  binom  11473  bcxmas  11478  isumshft  11479  isumnn0nn  11482  mertenslem2  11525  clim2prod  11528  prodfrecap  11535  prodeq2  11546  zproddc  11568  fprodseq  11572  fprodf1o  11577  prodsnf  11581  fprodfac  11604  fprodabs  11605  fprodconst  11609  fprod2d  11612  fprodrec  11618  fprodmodd  11630  efne0  11667  efexp  11671  demoivreALT  11762  moddvds  11787  gcddiv  12000  alginv  12027  algfx  12032  lcmneg  12054  lcmid  12060  lcmgcdeq  12063  divgcdcoprm0  12081  cncongr1  12083  cncongr2  12084  nn0gcdsq  12180  crth  12204  eulerthlema  12210  eulerthlemh  12211  pythagtriplem1  12245  pcqmul  12283  pcexp  12289  pcneg  12304  pcmpt  12321  pcfac  12328  1arith  12345  mgmidmo  12680  mgmlrid  12687  lidrideqd  12689  lidrididd  12690  grprinvlem  12693  grprinvd  12694  issgrp  12698  isnsgrp  12701  sgrpass  12703  sgrp1  12705  ismndd  12727  mndpropd  12730  mnd1  12734  mnd1id  12735  ismhm  12740  mhmpropd  12744  mhmlin  12745  mhmeql  12763  isgrp  12770  grppropd  12780  isgrpd2e  12783  dfgrp2  12789  isgrpid2  12800  grpidd2  12801  grpinvfvalg  12802  grpinvpropdg  12831  grpidssd  12832  grpinvssd  12833  grpsubrcan  12837  dfgrp3mlem  12854  grplactcnv  12858  mhmlem  12864  mulgnn0p1  12880  mulgaddcom  12892  mulginvcom  12893  mulgneg2  12902  mulgnnass  12903  mulgnn0ass  12904  mulgass  12905  mhmmulg  12909  iscmn  12920  cmnpropd  12922  iscmnd  12925  abladdsub4  12941  issrg  12971  srgmulgass  12995  srgpcomp  12996  srg1expzeq1  13001  isring  13006  iscrng2  13021  ringpropd  13040  ringinvnz1ne0  13049  mulgass2  13058  ring1  13059  opprnegg  13075  dvdsrd  13085  dvreq1  13133  txcnp  13431  cnmpt11  13443  cnmpt21  13451  cnmptcom  13458  isxms  13611  xmspropd  13637  bdmopn  13664  dvexp  13835  lgsne0  14099  nninffeq  14418
  Copyright terms: Public domain W3C validator