Theorem 3eqtr4a 1535

Description: A chained equality inference, useful for converting to definitions.

Hypotheses

Ref	Expression
3eqtr4a.1	⊢ A = B
3eqtr4a.2	⊢ (φ → C = A)
3eqtr4a.3	⊢ (φ → D = B)

Assertion

Ref	Expression
3eqtr4a	⊢ (φ → C = D)

Proof of Theorem 3eqtr4a

Step	Hyp	Ref	Expression
1		3eqtr4a.1	. . 3 ⊢ A = B
2	1	a1i 8	. 2 ⊢ (φ → A = B)
3		3eqtr4a.2	. 2 ⊢ (φ → C = A)
4		3eqtr4a.3	. 2 ⊢ (φ → D = B)
5	2, 3, 4	3eqtr4d 1520	1 ⊢ (φ → C = D)

Syntax hints:   → wi 3   = wceq 958

This theorem is referenced by:  ordunisuc 3095  unizlim 3119  dmsnop 3334  dmxpid 3339  fopabsn 3846  1stval2 4095  2ndval2 4096  oev2 4168  ecoprcom 4325  ecoprass 4326  ecoprdi 4327  xpmapenlem5 4506  unxpdomlem 4854  cardidm 4860  cardiun 4870  alephcard 4878  cardalephex 4897  cardcf 4923  eqneg 5806  zeot 6201  sq01t 6652  absexpt 6868  facp1t 6936  bcpasc 6969  binom 7072  efexpt 7372  sin01bndlem3 7470  infxpidmlem4 7556  alephadd 7584  grpsn 8120  ringsn 8159  ipid 8359  ipasslem1 8486  pjclem2 10119  cvmd 10246  symggrpi 10401  hmeogrp 10524  1ded 10642

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1472

Copyright terms: Public domain