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

Theorem 3eqtr2d 2226
Description: A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.)
Hypotheses
Ref Expression
3eqtr2d.1 (𝜑𝐴 = 𝐵)
3eqtr2d.2 (𝜑𝐶 = 𝐵)
3eqtr2d.3 (𝜑𝐶 = 𝐷)
Assertion
Ref Expression
3eqtr2d (𝜑𝐴 = 𝐷)

Proof of Theorem 3eqtr2d
StepHypRef Expression
1 3eqtr2d.1 . . 3 (𝜑𝐴 = 𝐵)
2 3eqtr2d.2 . . 3 (𝜑𝐶 = 𝐵)
31, 2eqtr4d 2223 . 2 (𝜑𝐴 = 𝐶)
4 3eqtr2d.3 . 2 (𝜑𝐶 = 𝐷)
53, 4eqtrd 2220 1 (𝜑𝐴 = 𝐷)
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:  fmptapd  5720  rdgisucinc  6399  ctm  7121  mulidnq  7401  ltrnqg  7432  recexprlem1ssl  7645  recexprlem1ssu  7646  ltmprr  7654  mulcmpblnrlemg  7752  caucvgsrlemoffcau  7810  negsub  8218  neg2sub  8230  divmuleqap  8687  divneg2ap  8706  qapne  9652  seqvalcd  10472  binom2  10645  bcpasc  10759  crim  10880  remullem  10893  max0addsup  11241  summodclem2a  11402  isum1p  11513  geo2sum  11535  cvgratz  11553  efi4p  11738  tanaddap  11760  addcos  11767  cos2tsin  11772  demoivreALT  11794  omeo  11916  sqgcd  12043  eulerthlemth  12245  pythagtriplem16  12292  fldivp1  12359  pockthlem  12367  4sqlem10  12398  grpinvid2  12949  imasgrp2  13004  mulgaddcomlem  13037  mulgmodid  13053  ablsubsub  13154  ablsubsub4  13155  opprunitd  13353  lmodfopne  13510  txrest  14047  limccnpcntop  14415  dvrecap  14448  cosq34lt1  14542  lgseisenlem1  14721
  Copyright terms: Public domain W3C validator