Theorem eqcoms 2207

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 2206	. 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 1372

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 1469  ax-gen 1471  ax-ext 2186

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

This theorem is referenced by:  gencbvex  2818  gencbval  2820  sbceq2a  3008  eqimss2  3247  uneqdifeqim  3545  tppreq3  3735  copsex2t  4288  copsex2g  4289  ordsoexmid  4609  0elsucexmid  4612  ordpwsucexmid  4617  cnveqb  5137  cnveq0  5138  relcoi1  5213  funtpg  5324  f0rn0  5469  fimadmfo  5506  f1ocnvfv  5847  f1ocnvfvb  5848  cbvfo  5853  cbvexfo  5854  brabvv  5990  ov6g  6083  ectocld  6687  ecoptocl  6708  phplem3  6950  f1dmvrnfibi  7045  f1vrnfibi  7046  updjud  7183  pr2ne  7299  nn0ind-raph  9489  nn01to3  9737  modqmuladd  10509  modqmuladdnn0  10511  fihashf1rn  10931  hashfzp1  10967  lswlgt0cl  11043  rennim  11255  xrmaxiflemcom  11502  m1expe  12152  m1expo  12153  m1exp1  12154  nn0o1gt2  12158  flodddiv4  12189  cncongr1  12367  m1dvdsndvds  12513  mgmsscl  13135  mndinvmod  13219  ringinvnzdiv  13754  txcn  14689  relogbcxpbap  15379  logbgcd1irr  15381  logbgcd1irraplemexp  15382  fsumdvdsmul  15405  zabsle1  15418  2lgslem1c  15509  2lgsoddprmlem3  15530  bj-inf2vnlem2  15840