Theorem eqcoms 2209

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 2208	. 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 1373

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 1471  ax-gen 1473  ax-ext 2188

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

This theorem is referenced by:  gencbvex  2821  gencbval  2823  sbceq2a  3013  eqimss2  3252  uneqdifeqim  3550  tppreq3  3741  copsex2t  4297  copsex2g  4298  ordsoexmid  4618  0elsucexmid  4621  ordpwsucexmid  4626  cnveqb  5147  cnveq0  5148  relcoi1  5223  funtpg  5334  f0rn0  5482  fimadmfo  5519  f1ocnvfv  5861  f1ocnvfvb  5862  cbvfo  5867  cbvexfo  5868  brabvv  6004  ov6g  6097  ectocld  6701  ecoptocl  6722  phplem3  6966  f1dmvrnfibi  7061  f1vrnfibi  7062  updjud  7199  pr2ne  7315  nn0ind-raph  9510  nn01to3  9758  modqmuladd  10533  modqmuladdnn0  10535  fihashf1rn  10955  hashfzp1  10991  lswlgt0cl  11068  wrd2ind  11199  rennim  11388  xrmaxiflemcom  11635  m1expe  12285  m1expo  12286  m1exp1  12287  nn0o1gt2  12291  flodddiv4  12322  cncongr1  12500  m1dvdsndvds  12646  mgmsscl  13268  mndinvmod  13352  ringinvnzdiv  13887  txcn  14822  relogbcxpbap  15512  logbgcd1irr  15514  logbgcd1irraplemexp  15515  fsumdvdsmul  15538  zabsle1  15551  2lgslem1c  15642  2lgsoddprmlem3  15663  bj-inf2vnlem2  16045