Theorem eqcoms 2199

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 2198	. 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 1364

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 1461  ax-gen 1463  ax-ext 2178

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

This theorem is referenced by:  gencbvex  2810  gencbval  2812  sbceq2a  3000  eqimss2  3239  uneqdifeqim  3537  tppreq3  3726  copsex2t  4279  copsex2g  4280  ordsoexmid  4599  0elsucexmid  4602  ordpwsucexmid  4607  cnveqb  5126  cnveq0  5127  relcoi1  5202  funtpg  5310  f0rn0  5455  fimadmfo  5492  f1ocnvfv  5829  f1ocnvfvb  5830  cbvfo  5835  cbvexfo  5836  brabvv  5972  ov6g  6065  ectocld  6669  ecoptocl  6690  phplem3  6924  f1dmvrnfibi  7019  f1vrnfibi  7020  updjud  7157  pr2ne  7271  nn0ind-raph  9460  nn01to3  9708  modqmuladd  10475  modqmuladdnn0  10477  fihashf1rn  10897  hashfzp1  10933  rennim  11184  xrmaxiflemcom  11431  m1expe  12081  m1expo  12082  m1exp1  12083  nn0o1gt2  12087  flodddiv4  12118  cncongr1  12296  m1dvdsndvds  12442  mgmsscl  13063  mndinvmod  13147  ringinvnzdiv  13682  txcn  14595  relogbcxpbap  15285  logbgcd1irr  15287  logbgcd1irraplemexp  15288  fsumdvdsmul  15311  zabsle1  15324  2lgslem1c  15415  2lgsoddprmlem3  15436  bj-inf2vnlem2  15701