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

Theorem eqtr4id 2193
 Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
Hypotheses
Ref Expression
eqtr4id.2
eqtr4id.1
Assertion
Ref Expression
eqtr4id

Proof of Theorem eqtr4id
StepHypRef Expression
1 eqtr4id.1 . 2
2 eqtr4id.2 . . 3
32eqcomi 2145 . 2
41, 3eqtr2di 2191 1
 Colors of variables: wff set class Syntax hints:   wi 4   wceq 1332 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 1424  ax-gen 1426  ax-4 1487  ax-17 1503  ax-ext 2123 This theorem depends on definitions:  df-bi 116  df-cleq 2134 This theorem is referenced by:  iftrue  3486  iffalse  3489  difprsn1  3669  dmmptg  5048  relcoi1  5082  funimacnv  5211  dmmptd  5265  dffv3g  5429  dfimafn  5482  fvco2  5502  isoini  5731  oprabco  6126  ixpconstg  6613  unfiexmid  6823  undifdc  6829  sbthlemi4  6865  sbthlemi5  6866  sbthlemi6  6867  supval2ti  6899  exmidfodomrlemim  7086  suplocexprlemex  7583  eqneg  8545  zeo  9209  fseq1p1m1  9934  seq3val  10291  seqvalcd  10292  hashfzo  10629  hashxp  10633  fsumconst  11284  modfsummod  11288  telfsumo  11296  mulgcd  11776  algcvg  11801  phiprmpw  11970  strslfv3  12079  uptx  12518  resubmet  12792
 Copyright terms: Public domain W3C validator