Theorem 3eqtr3a 2796

Description: A chained equality inference, useful for converting from definitions. (Contributed by Mario Carneiro, 6-Nov-2015.)

Hypotheses

Ref	Expression
3eqtr3a.1	⊢ 𝐴 = 𝐵
3eqtr3a.2	⊢ (𝜑 → 𝐴 = 𝐶)
3eqtr3a.3	⊢ (𝜑 → 𝐵 = 𝐷)

Assertion

Ref	Expression
3eqtr3a	⊢ (𝜑 → 𝐶 = 𝐷)

Proof of Theorem 3eqtr3a

Step	Hyp	Ref	Expression
1		3eqtr3a.2	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
2		3eqtr3a.1	. . 3 ⊢ 𝐴 = 𝐵
3		3eqtr3a.3	. . 3 ⊢ (𝜑 → 𝐵 = 𝐷)
4	2, 3	eqtrid 2784	. 2 ⊢ (𝜑 → 𝐴 = 𝐷)
5	1, 4	eqtr3d 2774	1 ⊢ (𝜑 → 𝐶 = 𝐷)

Syntax hints:   → wi 4   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724

This theorem is referenced by:  uneqin  4277  coi2  6259  foima  6807  f1imacnv  6846  fvsnun1  7176  fnsnsplit  7178  phplem2  9204  php3  9208  phplem4OLD  9216  php3OLD  9220  rankopb  9843  fin4en1  10300  fpwwe2  10634  winacard  10683  mul02lem1  11386  cnegex2  11392  crreczi  14187  hashinf  14291  hashcard  14311  cshw0  14740  cshwn  14743  sqrtneglem  15209  rlimresb  15505  bpoly3  15998  bpoly4  15999  sinhval  16093  coshval  16094  absefib  16137  efieq1re  16138  sadcaddlem  16394  sadaddlem  16403  qus0subgbas  19069  psgnsn  19382  odngen  19439  frlmup3  21346  mat0op  21912  restopnb  22670  cnmpt2t  23168  clmnegneg  24611  ncvspi  24664  volsup2  25113  plypf1  25717  pige3ALT  26020  sineq0  26024  eflog  26076  logef  26081  cxpsqrt  26202  dvcncxp1  26240  cubic2  26342  quart1  26350  asinsinlem  26385  asinsin  26386  2efiatan  26412  pclogsum  26707  lgsneg  26813  vc0  29814  vcm  29816  nvpi  29907  honegneg  31046  opsqrlem6  31385  sto1i  31476  mdexchi  31575  preiman0  31918  elrspunidl  32534  cnre2csqlem  32878  itgexpif  33606  subfacp1lem1  34158  rankaltopb  34939  poimirlem23  36499  dvtan  36526  dvasin  36560  heiborlem6  36672  trlcoat  39582  cdlemk54  39817  resubid  41277  sn-mul02  41309  iocunico  41945  relintab  42319  rfovcnvf1od  42740  ntrneifv3  42818  ntrneifv4  42821  clsneifv3  42846  clsneifv4  42847  neicvgfv  42857  snunioo1  44211  dvsinexp  44613  itgsubsticclem  44677  stirlinglem1  44776  fourierdlem80  44888  fourierdlem111  44919  sqwvfoura  44930  sqwvfourb  44931  fouriersw  44933  saliinclf  45028  smfco  45504  aacllem  47801