Theorem 3eqtr3a 2794

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 2782	. 2 ⊢ (𝜑 → 𝐴 = 𝐷)
5	1, 4	eqtr3d 2772	1 ⊢ (𝜑 → 𝐶 = 𝐷)

Syntax hints:   → wi 4   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727

This theorem is referenced by:  uneqin  4264  coi2  6252  foima  6795  f1imacnv  6834  fvsnun1  7174  fnsnsplit  7176  phplem2  9219  php3  9223  php3OLD  9233  rankopb  9866  fin4en1  10323  fpwwe2  10657  winacard  10706  mul02lem1  11411  cnegex2  11417  crreczi  14246  hashinf  14353  hashcard  14373  cshw0  14812  cshwn  14815  sqrtneglem  15285  rlimresb  15581  bpoly3  16074  bpoly4  16075  sinhval  16172  coshval  16173  absefib  16216  efieq1re  16217  sadcaddlem  16476  sadaddlem  16485  qus0subgbas  19181  psgnsn  19501  odngen  19558  frlmup3  21760  mat0op  22357  restopnb  23113  cnmpt2t  23611  clmnegneg  25055  ncvspi  25108  volsup2  25558  plypf1  26169  pige3ALT  26481  sineq0  26485  eflog  26537  logef  26542  cxpsqrt  26664  dvcncxp1  26704  cubic2  26810  quart1  26818  asinsinlem  26853  asinsin  26854  2efiatan  26880  pclogsum  27178  lgsneg  27284  vc0  30555  vcm  30557  nvpi  30648  honegneg  31787  opsqrlem6  32126  sto1i  32217  mdexchi  32316  fmptunsnop  32677  preiman0  32687  elrspunidl  33443  cnre2csqlem  33941  itgexpif  34638  subfacp1lem1  35201  rankaltopb  35997  poimirlem23  37667  dvtan  37694  dvasin  37728  heiborlem6  37840  trlcoat  40742  cdlemk54  40977  readvcot  42407  resubid  42451  sn-mul02  42483  iocunico  43235  relintab  43607  rfovcnvf1od  44028  ntrneifv3  44106  ntrneifv4  44109  clsneifv3  44134  clsneifv4  44135  neicvgfv  44145  snunioo1  45541  dvsinexp  45940  dvnprodlem1  45975  itgsubsticclem  46004  stirlinglem1  46103  fourierdlem80  46215  fourierdlem111  46246  sqwvfoura  46257  sqwvfourb  46258  fouriersw  46260  saliinclf  46355  smfco  46831  2oppf  49080  aacllem  49665