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  4608  0elsucexmid  4611  ordpwsucexmid  4616  cnveqb  5135  cnveq0  5136  relcoi1  5211  funtpg  5319  f0rn0  5464  fimadmfo  5501  f1ocnvfv  5838  f1ocnvfvb  5839  cbvfo  5844  cbvexfo  5845  brabvv  5981  ov6g  6074  ectocld  6678  ecoptocl  6699  phplem3  6933  f1dmvrnfibi  7028  f1vrnfibi  7029  updjud  7166  pr2ne  7282  nn0ind-raph  9472  nn01to3  9720  modqmuladd  10492  modqmuladdnn0  10494  fihashf1rn  10914  hashfzp1  10950  lswlgt0cl  11020  rennim  11232  xrmaxiflemcom  11479  m1expe  12129  m1expo  12130  m1exp1  12131  nn0o1gt2  12135  flodddiv4  12166  cncongr1  12344  m1dvdsndvds  12490  mgmsscl  13111  mndinvmod  13195  ringinvnzdiv  13730  txcn  14665  relogbcxpbap  15355  logbgcd1irr  15357  logbgcd1irraplemexp  15358  fsumdvdsmul  15381  zabsle1  15394  2lgslem1c  15485  2lgsoddprmlem3  15506  bj-inf2vnlem2  15771