Theorem eqcoms 2241

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 2240	. 2 |- ( B = A <-> A = B )
2		eqcoms.1	. 2 |- ( A = B -> ph )
3	1, 2	sylbi 121	1 |- ( B = A -> ph )

This proof depends on syntax axioms:   -> wi 4   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  gencbvex  2869  gencbval  2871  sbceq2a  3062  eqimss2  3303  uneqdifeqim  3613  tppreq3  3814  ifpprsnssdc  3820  copsex2t  4385  copsex2g  4386  ordsoexmid  4709  0elsucexmid  4712  ordpwsucexmid  4717  cnveqb  5243  cnveq0  5244  relcoi1  5319  funtpg  5432  f0rn0  5587  fimadmfo  5624  f1ssf1  5671  f1ocnvfv  5985  f1ocnvfvb  5986  cbvfo  5991  cbvexfo  5992  riotaeqimp  6063  brabvv  6134  ov6g  6227  ectocld  6875  ecoptocl  6896  phplem3  7155  f1dmvrnfibi  7258  f1vrnfibi  7259  updjud  7423  pr2ne  7539  nn0ind-raph  9768  nn01to3  10027  modqmuladd  10817  modqmuladdnn0  10819  fihashf1rn  11242  hashfzp1  11280  lswlgt0cl  11372  wrd2ind  11510  pfxccatin12lem2  11518  pfxccatin12lem3  11519  rennim  11783  xrmaxiflemcom  12033  m1expe  12684  m1expo  12685  m1exp1  12686  nn0o1gt2  12690  flodddiv4  12721  cncongr1  12899  m1dvdsndvds  13049  mgmsscl  13732  mndinvmod  13809  ringinvnzdiv  14406  txcn  15428  relogbcxpbap  16123  logbgcd1irr  16125  logbgcd1irraplemexp  16126  fsumdvdsmul  16207  zabsle1  16240  2lgslem1c  16331  2lgsoddprmlem3  16352  upgrpredgv  16509  usgredg2vlem2  16586  ushgredgedg  16589  ushgredgedgloop  16591  ifpsnprss  16706  upgrwlkvtxedg  16727  uspgr2wlkeq  16728  eupth2lem3lem3fi  16833  eupth2lem3lem4fi  16836  bj-inf2vnlem2  17119