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 1397

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 1495  ax-gen 1497  ax-ext 2213

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

This theorem is referenced by:  gencbvex  2850  gencbval  2852  sbceq2a  3042  eqimss2  3282  uneqdifeqim  3580  tppreq3  3774  ifpprsnssdc  3779  copsex2t  4337  copsex2g  4338  ordsoexmid  4660  0elsucexmid  4663  ordpwsucexmid  4668  cnveqb  5192  cnveq0  5193  relcoi1  5268  funtpg  5381  f0rn0  5531  fimadmfo  5568  f1ssf1  5615  f1ocnvfv  5919  f1ocnvfvb  5920  cbvfo  5925  cbvexfo  5926  riotaeqimp  5995  brabvv  6066  ov6g  6159  ectocld  6769  ecoptocl  6790  phplem3  7039  f1dmvrnfibi  7142  f1vrnfibi  7143  updjud  7280  pr2ne  7396  nn0ind-raph  9596  nn01to3  9850  modqmuladd  10627  modqmuladdnn0  10629  fihashf1rn  11049  hashfzp1  11087  lswlgt0cl  11165  wrd2ind  11303  pfxccatin12lem2  11311  pfxccatin12lem3  11312  rennim  11562  xrmaxiflemcom  11809  m1expe  12459  m1expo  12460  m1exp1  12461  nn0o1gt2  12465  flodddiv4  12496  cncongr1  12674  m1dvdsndvds  12820  mgmsscl  13443  mndinvmod  13527  ringinvnzdiv  14062  txcn  14998  relogbcxpbap  15688  logbgcd1irr  15690  logbgcd1irraplemexp  15691  fsumdvdsmul  15714  zabsle1  15727  2lgslem1c  15818  2lgsoddprmlem3  15839  upgrpredgv  15996  usgredg2vlem2  16073  ushgredgedg  16076  ushgredgedgloop  16078  ifpsnprss  16193  upgrwlkvtxedg  16214  uspgr2wlkeq  16215  bj-inf2vnlem2  16566