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

Theorem eqeq1d 2093
Description: Deduction from equality to equivalence of equalities. (Contributed by NM, 27-Dec-1993.)
Hypothesis
Ref Expression
eqeq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
eqeq1d  |-  ( ph  ->  ( A  =  C  <-> 
B  =  C ) )

Proof of Theorem eqeq1d
StepHypRef Expression
1 eqeq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 eqeq1 2091 . 2  |-  ( A  =  B  ->  ( A  =  C  <->  B  =  C ) )
31, 2syl 14 1  |-  ( ph  ->  ( A  =  C  <-> 
B  =  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103    = wceq 1287
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-gen 1381  ax-4 1443  ax-17 1462  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-cleq 2078
This theorem is referenced by:  rspcedeq1vd  2722  sbceq2g  2942  csbhypf  2955  csbiebt  2956  csbiebg  2959  dfss4st  3221  disjssun  3334  sneqrg  3589  preq12b  3597  preq12bg  3600  iin0r  3979  opthg  4039  opeqsn  4053  unisucg  4215  opthreg  4345  tfisi  4375  dmsnopg  4868  relcoi1  4928  iotaeq  4954  iotabi  4955  fneq1  5067  fnun  5085  fnresdisj  5089  fnimadisj  5099  fnimaeq0  5100  sbcfng  5124  foeq1  5192  foco  5206  fveqeq2d  5276  fvelimab  5323  fvun1  5333  fvmptdv2  5355  fneqeql  5370  dffo3  5409  fvsng  5456  fconstfvm  5476  eufnfv  5486  f1veqaeq  5509  dff13f  5510  f1elima  5513  foeqcnvco  5530  f1eqcocnv  5531  acexmidlemab  5607  eloprabga  5692  ovmpt2dv2  5735  ovi3  5738  ovelimab  5752  caovcang  5763  caovcan  5766  caovimo  5795  grprinvlem  5796  grpridd  5798  suppssfv  5809  suppssov1  5810  caofinvl  5834  op1stg  5878  op2ndg  5879  eqop  5904  reldm  5913  xporderlem  5953  tposfo2  5986  frec0g  6116  freccllem  6121  frecfcllem  6123  frecsuclem  6125  frecsuc  6126  nnm0r  6194  nnmord  6228  nnaordex  6238  nnawordex  6239  ereq1  6251  eqerlem  6275  mapsn  6399  endisj  6492  xpf1o  6512  mapxpen  6516  fidifsnen  6538  supelti  6641  updjudhcoinlf  6715  updjudhcoinrg  6716  updjud  6717  enomnilem  6738  finomni  6740  exmidomni  6742  fodjuomnilemm  6745  fodjuomnilem0  6746  fodjuomnilemres  6747  fodjuomni  6748  pm54.43  6762  exmidfodomrlemrALT  6773  addnidpig  6839  ltexpi  6840  dfplpq2  6857  dfmpq2  6858  recexnq  6893  recmulnqg  6894  ltexnqq  6911  halfnqq  6913  enq0tr  6937  nqnq0pi  6941  addnnnq0  6952  addlocpr  7039  ltexprlemru  7115  ltexpri  7116  lteupri  7120  prplnqu  7123  recexpr  7141  addsrpr  7235  mulsrpr  7236  00sr  7259  negexsr  7262  recexgt0sr  7263  srpospr  7272  prsrriota  7277  caucvgsrlemfv  7280  elrealeu  7311  axrnegex  7358  axprecex  7359  rereceu  7368  recriota  7369  nntopi  7373  axcaucvglemval  7376  axcaucvglemcau  7377  cnegexlem1  7601  cnegex  7604  cnegex2  7605  subval  7618  subadd  7629  subadd2  7630  subsub23  7631  addsubeq4  7641  subcan2  7651  negcon1  7678  subcan  7681  addrsub  7793  ltadd2  7841  recexre  7996  recexap  8061  muleqadd  8076  receuap  8077  divvalap  8080  divmulap  8081  rec11ap  8116  zdiv  8767  uzin  8983  icc0r  9276  fznlem  9387  fseq1m1p1  9439  1fv  9478  fzon  9505  fvinim0ffz  9580  ioo0  9599  ico0  9601  ioc0  9602  flqbi  9625  divfl0  9631  modq0  9664  modqmuladdnn0  9703  addmodlteq  9733  frecuzrdgtcl  9747  frecuzrdgfunlem  9754  iseqf1olemstep  9835  iseqf1olemp  9836  iseqid3s  9842  iseqid  9843  iseqid2  9844  iseqz  9846  mulreap  10194  rennim  10331  resqrexlemex  10354  rsqrmo  10356  resqrtcl  10358  rersqrtthlem  10359  sqrtsq2  10372  fisumcvg  10658  isumss  10671  divides  10680  dvdsval2  10681  nndivides  10685  dvds0lem  10688  dvds1lem  10689  dvds2lem  10690  negdvdsb  10694  muldvds1  10703  muldvds2  10704  dvdscmulr  10707  dvdsmulcr  10708  dvdstr  10715  dvdsabseq  10730  divconjdvds  10732  odd2np1lem  10754  odd2np1  10755  even2n  10756  oddm1even  10757  2tp1odd  10766  opeo  10779  omeo  10780  m1exp1  10783  divalgb  10807  gcdaddm  10857  gcdabs1  10862  bezout  10882  gcdmultiple  10891  gcdmultiplez  10892  rplpwr  10898  rppwr  10899  ialginv  10911  ialgcvga  10915  ialgfx  10916  eucalgval2  10917  coprmdvds  10956  qredeq  10960  qredeu  10961  divgcdcoprm0  10965  divgcdcoprmex  10966  cncongr1  10967  rpexp  11014  rpexp12i  11016  cncongrprm  11018  qnumdenbi  11052  phival  11071  phicl2  11072  dfphi2  11078  phiprmpw  11080  phimullem  11083  hashgcdlem  11085  peano4nninf  11341  nninfalllemn  11343  nninfalllem1  11344  nninfsellemdc  11347  nninfsellemeq  11351  nninfsellemqall  11352  nninfsellemeqinf  11353  nninfomnilem  11355  nninfomni  11356
  Copyright terms: Public domain W3C validator