Theorem eqcoms 2178

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 2177	. 2 |- ( B = A <-> A = B )
2		eqcoms.1	. 2 |- ( A = B -> ph )
3	1, 2	sylbi 121	1 |- ( B = A -> ph )

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 1445  ax-gen 1447  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-cleq 2168

This theorem is referenced by:  gencbvex  2781  gencbval  2783  sbceq2a  2971  eqimss2  3208  uneqdifeqim  3506  tppreq3  3692  copsex2t  4239  copsex2g  4240  ordsoexmid  4555  0elsucexmid  4558  ordpwsucexmid  4563  cnveqb  5076  cnveq0  5077  relcoi1  5152  funtpg  5259  f0rn0  5402  f1ocnvfv  5770  f1ocnvfvb  5771  cbvfo  5776  cbvexfo  5777  brabvv  5911  ov6g  6002  ectocld  6591  ecoptocl  6612  phplem3  6844  f1dmvrnfibi  6933  f1vrnfibi  6934  updjud  7071  pr2ne  7181  nn0ind-raph  9343  nn01to3  9590  modqmuladd  10336  modqmuladdnn0  10338  fihashf1rn  10736  hashfzp1  10772  rennim  10979  xrmaxiflemcom  11225  m1expe  11871  m1expo  11872  m1exp1  11873  nn0o1gt2  11877  flodddiv4  11906  cncongr1  12070  m1dvdsndvds  12215  mgmsscl  12646  mndinvmod  12709  ringinvnzdiv  13023  txcn  13346  relogbcxpbap  13954  logbgcd1irr  13956  logbgcd1irraplemexp  13957  zabsle1  13971  bj-inf2vnlem2  14283