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  5520  fimadmfo  5557  f1ocnvfv  5903  f1ocnvfvb  5904  cbvfo  5909  cbvexfo  5910  riotaeqimp  5979  brabvv  6050  ov6g  6143  ectocld  6748  ecoptocl  6769  phplem3  7015  f1dmvrnfibi  7111  f1vrnfibi  7112  updjud  7249  pr2ne  7365  nn0ind-raph  9564  nn01to3  9812  modqmuladd  10588  modqmuladdnn0  10590  fihashf1rn  11010  hashfzp1  11046  lswlgt0cl  11124  wrd2ind  11255  pfxccatin12lem2  11263  pfxccatin12lem3  11264  rennim  11513  xrmaxiflemcom  11760  m1expe  12410  m1expo  12411  m1exp1  12412  nn0o1gt2  12416  flodddiv4  12447  cncongr1  12625  m1dvdsndvds  12771  mgmsscl  13394  mndinvmod  13478  ringinvnzdiv  14013  txcn  14949  relogbcxpbap  15639  logbgcd1irr  15641  logbgcd1irraplemexp  15642  fsumdvdsmul  15665  zabsle1  15678  2lgslem1c  15769  2lgsoddprmlem3  15790  upgrpredgv  15944  usgredg2vlem2  16021  ushgredgedg  16024  ushgredgedgloop  16026  ifpsnprss  16054  upgrwlkvtxedg  16075  uspgr2wlkeq  16076  bj-inf2vnlem2  16334