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

Theorem eqcoms 2118
Description: Inference applying commutative law for class equality to an antecedent. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
eqcoms.1 (𝐴 = 𝐵𝜑)
Assertion
Ref Expression
eqcoms (𝐵 = 𝐴𝜑)

Proof of Theorem eqcoms
StepHypRef Expression
1 eqcom 2117 . 2 (𝐵 = 𝐴𝐴 = 𝐵)
2 eqcoms.1 . 2 (𝐴 = 𝐵𝜑)
31, 2sylbi 120 1 (𝐵 = 𝐴𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1314
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 1406  ax-gen 1408  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-cleq 2108
This theorem is referenced by:  gencbvex  2704  gencbval  2706  sbceq2a  2890  eqimss2  3120  uneqdifeqim  3416  tppreq3  3594  copsex2t  4135  copsex2g  4136  ordsoexmid  4445  0elsucexmid  4448  ordpwsucexmid  4453  cnveqb  4962  cnveq0  4963  relcoi1  5038  funtpg  5142  f0rn0  5285  f1ocnvfv  5646  f1ocnvfvb  5647  cbvfo  5652  cbvexfo  5653  brabvv  5783  ov6g  5874  ectocld  6461  ecoptocl  6482  phplem3  6714  f1dmvrnfibi  6798  f1vrnfibi  6799  updjud  6933  pr2ne  7014  nn0ind-raph  9122  nn01to3  9361  modqmuladd  10090  modqmuladdnn0  10092  fihashf1rn  10486  hashfzp1  10521  rennim  10725  xrmaxiflemcom  10969  m1expe  11503  m1expo  11504  m1exp1  11505  nn0o1gt2  11509  flodddiv4  11538  cncongr1  11691  txcn  12350  bj-inf2vnlem2  13003
  Copyright terms: Public domain W3C validator