Theorem eqcoms 2232

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 2231	. 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 1395

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 1493  ax-gen 1495  ax-ext 2211

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

This theorem is referenced by:  gencbvex  2847  gencbval  2849  sbceq2a  3039  eqimss2  3279  uneqdifeqim  3577  tppreq3  3769  copsex2t  4330  copsex2g  4331  ordsoexmid  4653  0elsucexmid  4656  ordpwsucexmid  4661  cnveqb  5183  cnveq0  5184  relcoi1  5259  funtpg  5371  f0rn0  5519  fimadmfo  5556  f1ocnvfv  5902  f1ocnvfvb  5903  cbvfo  5908  cbvexfo  5909  riotaeqimp  5978  brabvv  6049  ov6g  6142  ectocld  6746  ecoptocl  6767  phplem3  7011  f1dmvrnfibi  7107  f1vrnfibi  7108  updjud  7245  pr2ne  7361  nn0ind-raph  9560  nn01to3  9808  modqmuladd  10583  modqmuladdnn0  10585  fihashf1rn  11005  hashfzp1  11041  lswlgt0cl  11119  wrd2ind  11250  pfxccatin12lem2  11258  pfxccatin12lem3  11259  rennim  11508  xrmaxiflemcom  11755  m1expe  12405  m1expo  12406  m1exp1  12407  nn0o1gt2  12411  flodddiv4  12442  cncongr1  12620  m1dvdsndvds  12766  mgmsscl  13389  mndinvmod  13473  ringinvnzdiv  14008  txcn  14943  relogbcxpbap  15633  logbgcd1irr  15635  logbgcd1irraplemexp  15636  fsumdvdsmul  15659  zabsle1  15672  2lgslem1c  15763  2lgsoddprmlem3  15784  upgrpredgv  15938  usgredg2vlem2  16015  ushgredgedg  16018  ushgredgedgloop  16020  ifpsnprss  16040  bj-inf2vnlem2  16292