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

Theorem 3eqtr3a 2227
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
StepHypRef Expression
1 3eqtr3a.2 . 2 (𝜑𝐴 = 𝐶)
2 3eqtr3a.1 . . 3 𝐴 = 𝐵
3 3eqtr3a.3 . . 3 (𝜑𝐵 = 𝐷)
42, 3eqtrid 2215 . 2 (𝜑𝐴 = 𝐷)
51, 4eqtr3d 2205 1 (𝜑𝐶 = 𝐷)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1348
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 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152
This theorem depends on definitions:  df-bi 116  df-cleq 2163
This theorem is referenced by:  uneqin  3378  coi2  5127  foima  5425  f1imacnv  5459  fvsnun2  5694  fnsnsplitdc  6484  phplem4  6833  phplem4on  6845  halfnqq  7372  resqrexlemcalc1  10978  absefib  11733  efieq1re  11734  restopnb  12975  cnmpt2t  13087  reeflog  13578  rpcxpsqrt  13636
  Copyright terms: Public domain W3C validator