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

Theorem 3eqtr3a 2234
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 2222 . 2 (𝜑𝐴 = 𝐷)
51, 4eqtr3d 2212 1 (𝜑𝐶 = 𝐷)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1353
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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-cleq 2170
This theorem is referenced by:  uneqin  3386  coi2  5145  foima  5443  f1imacnv  5478  fvsnun2  5714  fnsnsplitdc  6505  phplem4  6854  phplem4on  6866  halfnqq  7408  resqrexlemcalc1  11018  absefib  11773  efieq1re  11774  restopnb  13612  cnmpt2t  13724  reeflog  14215  rpcxpsqrt  14273
  Copyright terms: Public domain W3C validator