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

Theorem 3eqtr3a 2196
Description: A chained equality inference, useful for converting from definitions. (Contributed by Mario Carneiro, 6-Nov-2015.)
Hypotheses
Ref Expression
3eqtr3a.1  |-  A  =  B
3eqtr3a.2  |-  ( ph  ->  A  =  C )
3eqtr3a.3  |-  ( ph  ->  B  =  D )
Assertion
Ref Expression
3eqtr3a  |-  ( ph  ->  C  =  D )

Proof of Theorem 3eqtr3a
StepHypRef Expression
1 3eqtr3a.2 . 2  |-  ( ph  ->  A  =  C )
2 3eqtr3a.1 . . 3  |-  A  =  B
3 3eqtr3a.3 . . 3  |-  ( ph  ->  B  =  D )
42, 3syl5eq 2184 . 2  |-  ( ph  ->  A  =  D )
51, 4eqtr3d 2174 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1331
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-cleq 2132
This theorem is referenced by:  uneqin  3327  coi2  5055  foima  5350  f1imacnv  5384  fvsnun2  5618  fnsnsplitdc  6401  phplem4  6749  phplem4on  6761  halfnqq  7225  resqrexlemcalc1  10793  absefib  11484  efieq1re  11485  restopnb  12360  cnmpt2t  12472  reeflog  12955
  Copyright terms: Public domain W3C validator