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

Theorem eqeq1d 2064
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 2062 . 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 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:  rspcedeq1vd  2681  sbceq2g  2900  csbhypf  2913  csbiebt  2914  csbiebg  2917  disjssun  3313  sneqrg  3561  preq12b  3569  preq12bg  3572  iin0r  3950  opthg  4003  opeqsn  4017  unisucg  4179  opthreg  4308  tfisi  4338  dmsnopg  4820  relcoi1  4877  iotaeq  4903  iotabi  4904  fneq1  5015  fnun  5033  fnresdisj  5037  fnimadisj  5047  fnimaeq0  5048  sbcfng  5072  foeq1  5130  foco  5144  fvelimab  5257  fvun1  5267  fvmptdv2  5288  fneqeql  5303  dffo3  5342  fvsng  5387  fconstfvm  5407  eufnfv  5417  f1veqaeq  5436  dff13f  5437  f1elima  5440  foeqcnvco  5458  f1eqcocnv  5459  acexmidlemab  5534  eloprabga  5619  ovmpt2dv2  5662  ovi3  5665  ovelimab  5679  caovcang  5690  caovcan  5693  caovimo  5722  grprinvlem  5723  grpridd  5725  suppssfv  5736  suppssov1  5737  caofinvl  5761  op1stg  5805  op2ndg  5806  eqop  5831  reldm  5840  xporderlem  5880  tposfo2  5913  frec0g  6014  frecsuclem3  6021  frecsuc  6022  nnm0r  6089  nnmord  6121  nnaordex  6131  nnawordex  6132  ereq1  6144  eqerlem  6168  endisj  6329  fidifsnen  6362  addnidpig  6492  ltexpi  6493  dfplpq2  6510  dfmpq2  6511  recexnq  6546  recmulnqg  6547  ltexnqq  6564  halfnqq  6566  enq0tr  6590  nqnq0pi  6594  addnnnq0  6605  addlocpr  6692  ltexprlemru  6768  ltexpri  6769  lteupri  6773  prplnqu  6776  recexpr  6794  addsrpr  6888  mulsrpr  6889  00sr  6912  negexsr  6915  recexgt0sr  6916  srpospr  6925  prsrriota  6930  caucvgsrlemfv  6933  elrealeu  6964  axrnegex  7011  axprecex  7012  rereceu  7021  recriota  7022  nntopi  7026  axcaucvglemval  7029  axcaucvglemcau  7030  cnegexlem1  7249  cnegex  7252  cnegex2  7253  subval  7266  subadd  7277  subadd2  7278  subsub23  7279  addsubeq4  7289  subcan2  7299  negcon1  7326  subcan  7329  addrsub  7441  ltadd2  7488  recexre  7643  recexap  7708  muleqadd  7723  receuap  7724  divvalap  7727  divmulap  7728  rec11ap  7761  zdiv  8386  uzin  8601  icc0r  8896  fznlem  9007  fseq1m1p1  9059  1fv  9098  fzon  9124  fvinim0ffz  9198  ioo0  9216  ico0  9218  ioc0  9219  flqbi  9240  divfl0  9246  modq0  9279  modqmuladdnn0  9318  addmodlteq  9348  frecuzrdgfn  9362  iseqid3s  9410  iseqid  9411  iseqz  9413  mulreap  9692  rennim  9829  resqrexlemex  9852  rsqrmo  9854  resqrtcl  9856  rersqrtthlem  9857  sqrtsq2  9870  divides  10110  dvdsval2  10111  nndivides  10115  dvds0lem  10118  dvds1lem  10119  dvds2lem  10120  negdvdsb  10124  muldvds1  10132  muldvds2  10133  dvdscmulr  10136  dvdsmulcr  10137  dvdstr  10144  dvdsabseq  10159  divconjdvds  10161  odd2np1lem  10183  odd2np1  10184  even2n  10185  oddm1even  10186  2tp1odd  10196  opeo  10209  omeo  10210  m1exp1  10213  divalgb  10237  ialginv  10269  ialgcvga  10273  ialgfx  10274
  Copyright terms: Public domain W3C validator