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

Theorem eqcoms 2143
 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 2142 . 2 (𝐵 = 𝐴𝐴 = 𝐵)
2 eqcoms.1 . 2 (𝐴 = 𝐵𝜑)
31, 2sylbi 120 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-ext 2122 This theorem depends on definitions:  df-bi 116  df-cleq 2133 This theorem is referenced by:  gencbvex  2736  gencbval  2738  sbceq2a  2924  eqimss2  3158  uneqdifeqim  3454  tppreq3  3635  copsex2t  4176  copsex2g  4177  ordsoexmid  4486  0elsucexmid  4489  ordpwsucexmid  4494  cnveqb  5004  cnveq0  5005  relcoi1  5080  funtpg  5184  f0rn0  5327  f1ocnvfv  5690  f1ocnvfvb  5691  cbvfo  5696  cbvexfo  5697  brabvv  5827  ov6g  5918  ectocld  6505  ecoptocl  6526  phplem3  6758  f1dmvrnfibi  6845  f1vrnfibi  6846  updjud  6980  pr2ne  7071  nn0ind-raph  9215  nn01to3  9459  modqmuladd  10193  modqmuladdnn0  10195  fihashf1rn  10590  hashfzp1  10625  rennim  10829  xrmaxiflemcom  11073  m1expe  11655  m1expo  11656  m1exp1  11657  nn0o1gt2  11661  flodddiv4  11690  cncongr1  11843  txcn  12506  relogbcxpbap  13113  logbgcd1irr  13115  logbgcd1irraplemexp  13116  bj-inf2vnlem2  13373
 Copyright terms: Public domain W3C validator