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

Theorem eqcoms 2180
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 2179 . 2 (𝐵 = 𝐴𝐴 = 𝐵)
2 eqcoms.1 . 2 (𝐴 = 𝐵𝜑)
31, 2sylbi 121 1 (𝐵 = 𝐴𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1353
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 1447  ax-gen 1449  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-cleq 2170
This theorem is referenced by:  gencbvex  2783  gencbval  2785  sbceq2a  2973  eqimss2  3210  uneqdifeqim  3508  tppreq3  3694  copsex2t  4241  copsex2g  4242  ordsoexmid  4557  0elsucexmid  4560  ordpwsucexmid  4565  cnveqb  5079  cnveq0  5080  relcoi1  5155  funtpg  5262  f0rn0  5405  f1ocnvfv  5773  f1ocnvfvb  5774  cbvfo  5779  cbvexfo  5780  brabvv  5914  ov6g  6005  ectocld  6594  ecoptocl  6615  phplem3  6847  f1dmvrnfibi  6936  f1vrnfibi  6937  updjud  7074  pr2ne  7184  nn0ind-raph  9346  nn01to3  9593  modqmuladd  10339  modqmuladdnn0  10341  fihashf1rn  10739  hashfzp1  10775  rennim  10982  xrmaxiflemcom  11228  m1expe  11874  m1expo  11875  m1exp1  11876  nn0o1gt2  11880  flodddiv4  11909  cncongr1  12073  m1dvdsndvds  12218  mgmsscl  12659  mndinvmod  12723  ringinvnzdiv  13040  txcn  13408  relogbcxpbap  14016  logbgcd1irr  14018  logbgcd1irraplemexp  14019  zabsle1  14033  bj-inf2vnlem2  14345
  Copyright terms: Public domain W3C validator