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  ifpprsnssdc  3774  copsex2t  4331  copsex2g  4332  ordsoexmid  4654  0elsucexmid  4657  ordpwsucexmid  4662  cnveqb  5184  cnveq0  5185  relcoi1  5260  funtpg  5372  f0rn0  5522  fimadmfo  5559  f1ocnvfv  5909  f1ocnvfvb  5910  cbvfo  5915  cbvexfo  5916  riotaeqimp  5985  brabvv  6056  ov6g  6149  ectocld  6756  ecoptocl  6777  phplem3  7023  f1dmvrnfibi  7122  f1vrnfibi  7123  updjud  7260  pr2ne  7376  nn0ind-raph  9575  nn01to3  9824  modqmuladd  10600  modqmuladdnn0  10602  fihashf1rn  11022  hashfzp1  11059  lswlgt0cl  11137  wrd2ind  11270  pfxccatin12lem2  11278  pfxccatin12lem3  11279  rennim  11528  xrmaxiflemcom  11775  m1expe  12425  m1expo  12426  m1exp1  12427  nn0o1gt2  12431  flodddiv4  12462  cncongr1  12640  m1dvdsndvds  12786  mgmsscl  13409  mndinvmod  13493  ringinvnzdiv  14028  txcn  14964  relogbcxpbap  15654  logbgcd1irr  15656  logbgcd1irraplemexp  15657  fsumdvdsmul  15680  zabsle1  15693  2lgslem1c  15784  2lgsoddprmlem3  15805  upgrpredgv  15959  usgredg2vlem2  16036  ushgredgedg  16039  ushgredgedgloop  16041  ifpsnprss  16084  upgrwlkvtxedg  16105  uspgr2wlkeq  16106  bj-inf2vnlem2  16389