Theorem eqcoms 2234

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 2233	. 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 1398

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 1496  ax-gen 1498  ax-ext 2213

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

This theorem is referenced by:  gencbvex  2851  gencbval  2853  sbceq2a  3043  eqimss2  3283  uneqdifeqim  3582  tppreq3  3778  ifpprsnssdc  3783  copsex2t  4343  copsex2g  4344  ordsoexmid  4666  0elsucexmid  4669  ordpwsucexmid  4674  cnveqb  5199  cnveq0  5200  relcoi1  5275  funtpg  5388  f0rn0  5540  fimadmfo  5577  f1ssf1  5624  f1ocnvfv  5930  f1ocnvfvb  5931  cbvfo  5936  cbvexfo  5937  riotaeqimp  6006  brabvv  6077  ov6g  6170  ectocld  6813  ecoptocl  6834  phplem3  7083  f1dmvrnfibi  7186  f1vrnfibi  7187  updjud  7324  pr2ne  7440  nn0ind-raph  9641  nn01to3  9895  modqmuladd  10674  modqmuladdnn0  10676  fihashf1rn  11096  hashfzp1  11134  lswlgt0cl  11215  wrd2ind  11353  pfxccatin12lem2  11361  pfxccatin12lem3  11362  rennim  11625  xrmaxiflemcom  11872  m1expe  12523  m1expo  12524  m1exp1  12525  nn0o1gt2  12529  flodddiv4  12560  cncongr1  12738  m1dvdsndvds  12884  mgmsscl  13507  mndinvmod  13591  ringinvnzdiv  14127  txcn  15069  relogbcxpbap  15759  logbgcd1irr  15761  logbgcd1irraplemexp  15762  fsumdvdsmul  15788  zabsle1  15801  2lgslem1c  15892  2lgsoddprmlem3  15913  upgrpredgv  16070  usgredg2vlem2  16147  ushgredgedg  16150  ushgredgedgloop  16152  ifpsnprss  16267  upgrwlkvtxedg  16288  uspgr2wlkeq  16289  eupth2lem3lem3fi  16394  eupth2lem3lem4fi  16397  bj-inf2vnlem2  16670