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  3238  uneqdifeqim  3536  tppreq3  3725  copsex2t  4278  copsex2g  4279  ordsoexmid  4598  0elsucexmid  4601  ordpwsucexmid  4606  cnveqb  5125  cnveq0  5126  relcoi1  5201  funtpg  5309  f0rn0  5452  fimadmfo  5489  f1ocnvfv  5826  f1ocnvfvb  5827  cbvfo  5832  cbvexfo  5833  brabvv  5968  ov6g  6061  ectocld  6660  ecoptocl  6681  phplem3  6915  f1dmvrnfibi  7010  f1vrnfibi  7011  updjud  7148  pr2ne  7259  nn0ind-raph  9443  nn01to3  9691  modqmuladd  10458  modqmuladdnn0  10460  fihashf1rn  10880  hashfzp1  10916  rennim  11167  xrmaxiflemcom  11414  m1expe  12064  m1expo  12065  m1exp1  12066  nn0o1gt2  12070  flodddiv4  12101  cncongr1  12271  m1dvdsndvds  12417  mgmsscl  13004  mndinvmod  13086  ringinvnzdiv  13606  txcn  14511  relogbcxpbap  15201  logbgcd1irr  15203  logbgcd1irraplemexp  15204  fsumdvdsmul  15227  zabsle1  15240  2lgslem1c  15331  2lgsoddprmlem3  15352  bj-inf2vnlem2  15617