Theorem eqtrid 2789

Description: An equality transitivity deduction. (Contributed by NM, 21-Jun-1993.)

Hypotheses

Ref	Expression
eqtrid.1	⊢ 𝐴 = 𝐵
eqtrid.2	⊢ (𝜑 → 𝐵 = 𝐶)

Assertion

Ref	Expression
eqtrid	⊢ (𝜑 → 𝐴 = 𝐶)

Proof of Theorem eqtrid

Step	Hyp	Ref	Expression
1		eqtrid.1	. . 3 ⊢ 𝐴 = 𝐵
2	1	a1i 11	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
3		eqtrid.2	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	2, 3	eqtrd 2777	1 ⊢ (𝜑 → 𝐴 = 𝐶)

Syntax hints:   → wi 4   = wceq 1543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2729

This theorem is referenced by:  eqtr2id  2791  eqtr3id  2792  3eqtr3a  2802  3eqtr4g  2803  rabeqcda  3405  csbtt  3828  csbied  3849  csbie2g  3854  ss2abdv  3977  rabbi2dva  4132  csbvarg  4346  csbsng  4624  csbprg  4625  disjpr2  4629  disjprsn  4630  disjtpsn  4631  disjtp2  4632  rabsnif  4639  prprc2  4682  difprsn2  4714  difsnid  4723  dfopg  4782  csbopg  4802  opprc  4807  csbuni  4850  intsng  4896  riinn0  4991  iinxsng  4996  iunxprg  5004  propeqop  5390  csbmpt12  5438  xpriindi  5705  relop  5719  dmxp  5798  riinint  5837  csbres  5854  resabs1  5881  resabs2  5883  xpssres  5888  dmressnsn  5893  resopab2  5904  imasng  5951  djudisj  6030  rnxp  6033  xpima  6045  xpima1  6046  xpima2  6047  dmsnsnsn  6083  rnsnopg  6084  rnpropg  6085  mptiniseg  6102  dfco2a  6110  relcoi2  6140  relcoi1  6141  unixp  6145  predep  6188  onfr  6252  iotaval  6354  iotanul  6358  funtp  6437  fnun  6490  fnresdisj  6497  fnima  6508  fnimaeq0  6511  fresaunres2  6591  fresaunres1  6592  fcoi1  6593  focofo  6646  f1orescnv  6676  foun  6679  resdif  6681  f1oprswap  6704  tz6.12-2  6706  fveu  6707  rnfvprc  6711  tz6.12-1  6739  csbfv12  6760  csbfv2g  6761  fvun  6801  fvun2  6803  fvopab3ig  6814  fvmptnf  6840  fvopab5  6850  intpreima  6890  fimacnvinrn  6892  fimacnvinrn2  6893  fveqressseq  6900  f1oresrab  6942  xpprsng  6955  residpr  6958  funsneqopb  6967  ressnop0  6968  fvunsn  6994  fsnunfv  7002  fvpr1  7005  fvpr2  7006  fvpr1g  7007  fvpr2g  7008  fvtp1  7010  fvtp2  7011  fvtp3  7012  fvtp1g  7013  fvtp2g  7014  fvtp3g  7015  tpres  7016  rnmptc  7022  fpropnf1  7079  f12dfv  7084  f13dfv  7085  nvof1o  7091  fveqf1o  7113  f1ofvswap  7116  f1oiso2  7161  riotaund  7210  ovprc  7251  csbov12g  7257  0mpo0  7294  resoprab2  7329  fnoprabg  7333  ovidig  7351  ovigg  7354  fvmpopr2d  7370  ov6g  7372  ovconst2  7388  nssdmovg  7390  ndmovg  7391  offval2f  7483  offval2  7488  orduniss2  7612  1stnpr  7765  2ndnpr  7766  ot1stg  7775  ot2ndg  7776  ot3rdg  7777  opabn1stprc  7828  brovpreldm  7857  bropopvvv  7858  bropfvvvvlem  7859  fmpoco  7863  curry1  7872  curry2  7875  fparlem3  7882  fparlem4  7883  fnwelem  7898  suppsnop  7920  tpostpos2  7989  mpocurryd  8011  frrlem4  8030  frrlem12  8038  wfrlem4  8058  wfrlem13  8067  tz7.44-2  8143  tz7.44-3  8144  rdgsucmptnf  8165  rdglim2  8168  fr0g  8171  frsucmptn  8174  seqom0g  8192  oa1suc  8258  om1  8270  oe1  8272  oarec  8290  oacomf1o  8293  nnm1  8377  nnm2  8378  dfec2  8394  errn  8413  ralxpmap  8577  ixpsnval  8581  ixpint  8606  domunsncan  8745  enfixsn  8754  domunsn  8796  fodomr  8797  domss2  8805  mapen  8810  xpmapenlem  8813  phplem2  8826  findcard2  8842  unxpdomlem1  8882  findcard2OLD  8913  domunfican  8944  mapfien  9024  marypha1lem  9049  marypha2lem4  9054  supval2  9071  supsn  9088  eqinf  9100  infval  9102  infsn  9121  infempty  9123  ordtypecbv  9133  ordtypelem3  9136  oi0  9144  wemapso2  9169  brwdom2  9189  infdifsn  9272  cantnfs  9281  cantnfval  9283  cantnflt  9287  cantnff  9289  cantnfp1  9296  oemapso  9297  wemapwe  9312  cnfcomlem  9314  cnfcom2lem  9316  cnfcom3lem  9318  trpredtr  9335  trpredmintr  9336  trpred0  9337  trpredrec  9342  rankxplim2  9496  infxpenlem  9627  infxpenc  9632  infxpenc2lem1  9633  fseqenlem1  9638  dfac12r  9760  kmlem11  9774  onadju  9807  ackbij1lem1  9834  ackbij1lem2  9835  ackbij1lem14  9847  ackbij1lem16  9849  ackbij1lem18  9851  ackbij2lem3  9855  fictb  9859  cfsmolem  9884  cfsmo  9885  infpssrlem1  9917  enfin2i  9935  fin23lem19  9950  fin23lem30  9956  isf32lem4  9970  isf32lem6  9972  isf32lem7  9973  isf32lem8  9974  isf34lem7  9993  isf34lem6  9994  fin1a2lem11  10024  ituniiun  10036  hsmexlem2  10041  hsmexlem4  10043  domtriomlem  10056  domtriom  10057  axdc3lem4  10067  zorn2g  10117  axdc  10135  fpwwe2lem12  10256  fpwwe  10260  canthwelem  10264  canthp1lem1  10266  pwfseqlem2  10273  pwfseqlem3  10274  wunex2  10352  wuncval2  10361  nqereu  10543  recrecnq  10581  ltaddnq  10588  halfnq  10590  ltrnq  10593  archnq  10594  addclprlem1  10630  addclprlem2  10631  mulclprlem  10633  distrlem4pr  10640  1idpr  10643  prlem934  10647  ltexprlem7  10656  ltaprlem  10658  prlem936  10661  mulcmpblnrlem  10684  0idsr  10711  1idsr  10712  recexsrlem  10717  sqgt0sr  10720  map2psrpr  10724  mulresr  10753  ax1rid  10775  axcnre  10778  ssxr  10902  addid2  11015  negid  11125  subneg  11127  negneg  11128  dfinfre  11813  infrenegsup  11815  2times  11966  rpnnen1  12579  rexneg  12801  xaddpnf2  12817  xaddmnf2  12819  x2times  12889  supxrmnf  12907  prunioo  13069  ioojoin  13071  fzpreddisj  13161  fseq1p1m1  13186  prednn  13235  prednn0  13236  fz0add1fz1  13312  quoremz  13428  quoremnn0ALT  13430  intfracq  13432  uzenom  13537  axdc4uzlem  13556  mptnn0fsuppd  13571  seq1i  13588  seqf1olem2  13616  seqof  13633  sqval  13687  iexpcyc  13775  binom3  13791  faclbnd  13856  faclbnd2  13857  bcn1  13879  hashkf  13898  hashgval  13899  hashdom  13946  hashxplem  14000  hashfun  14004  hashbclem  14016  hashbc  14017  hashf1lem1  14020  hashf1lem1OLD  14021  hashf1lem2  14022  fz1isolem  14027  csbwrdg  14099  ccatlid  14143