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

Theorem 3eqtr3a 2244
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, 3eqtrid 2232 . 2  |-  ( ph  ->  A  =  D )
51, 4eqtr3d 2222 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1363
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1457  ax-gen 1459  ax-4 1520  ax-17 1536  ax-ext 2169
This theorem depends on definitions:  df-bi 117  df-cleq 2180
This theorem is referenced by:  uneqin  3398  coi2  5157  foima  5455  f1imacnv  5490  fvsnun2  5727  fnsnsplitdc  6520  phplem4  6869  phplem4on  6881  halfnqq  7423  resqrexlemcalc1  11037  absefib  11792  efieq1re  11793  restopnb  14034  cnmpt2t  14146  reeflog  14637  rpcxpsqrt  14695
  Copyright terms: Public domain W3C validator