Theorem eqcoms 2168

Description: Inference applying commutative law for class equality to an antecedent. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
eqcoms.1	|- ( A = B -> ph )

Assertion

Ref	Expression
eqcoms	|- ( B = A -> ph )

Proof of Theorem eqcoms

Step	Hyp	Ref	Expression
1		eqcom 2167	. 2 |- ( B = A <-> A = B )
2		eqcoms.1	. 2 |- ( A = B -> ph )
3	1, 2	sylbi 120	1 |- ( B = A -> ph )

Syntax hints:   -> wi 4   = wceq 1343

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 1435  ax-gen 1437  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158

This theorem is referenced by:  gencbvex  2771  gencbval  2773  sbceq2a  2960  eqimss2  3196  uneqdifeqim  3493  tppreq3  3678  copsex2t  4222  copsex2g  4223  ordsoexmid  4538  0elsucexmid  4541  ordpwsucexmid  4546  cnveqb  5058  cnveq0  5059  relcoi1  5134  funtpg  5238  f0rn0  5381  f1ocnvfv  5746  f1ocnvfvb  5747  cbvfo  5752  cbvexfo  5753  brabvv  5884  ov6g  5975  ectocld  6563  ecoptocl  6584  phplem3  6816  f1dmvrnfibi  6905  f1vrnfibi  6906  updjud  7043  pr2ne  7144  nn0ind-raph  9304  nn01to3  9551  modqmuladd  10297  modqmuladdnn0  10299  fihashf1rn  10698  hashfzp1  10733  rennim  10940  xrmaxiflemcom  11186  m1expe  11832  m1expo  11833  m1exp1  11834  nn0o1gt2  11838  flodddiv4  11867  cncongr1  12031  m1dvdsndvds  12176  txcn  12875  relogbcxpbap  13483  logbgcd1irr  13485  logbgcd1irraplemexp  13486  zabsle1  13500  bj-inf2vnlem2  13813