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

Theorem eqcoms 2120
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 2119 . 2 (𝐵 = 𝐴𝐴 = 𝐵)
2 eqcoms.1 . 2 (𝐴 = 𝐵𝜑)
31, 2sylbi 120 1 (𝐵 = 𝐴𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1316
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 1408  ax-gen 1410  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-cleq 2110
This theorem is referenced by:  gencbvex  2706  gencbval  2708  sbceq2a  2892  eqimss2  3122  uneqdifeqim  3418  tppreq3  3596  copsex2t  4137  copsex2g  4138  ordsoexmid  4447  0elsucexmid  4450  ordpwsucexmid  4455  cnveqb  4964  cnveq0  4965  relcoi1  5040  funtpg  5144  f0rn0  5287  f1ocnvfv  5648  f1ocnvfvb  5649  cbvfo  5654  cbvexfo  5655  brabvv  5785  ov6g  5876  ectocld  6463  ecoptocl  6484  phplem3  6716  f1dmvrnfibi  6800  f1vrnfibi  6801  updjud  6935  pr2ne  7016  nn0ind-raph  9136  nn01to3  9377  modqmuladd  10107  modqmuladdnn0  10109  fihashf1rn  10503  hashfzp1  10538  rennim  10742  xrmaxiflemcom  10986  m1expe  11523  m1expo  11524  m1exp1  11525  nn0o1gt2  11529  flodddiv4  11558  cncongr1  11711  txcn  12371  bj-inf2vnlem2  13096
  Copyright terms: Public domain W3C validator