Theorem eqcoms 2142

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

Syntax hints:   -> wi 4   = wceq 1331

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-cleq 2132

This theorem is referenced by:  gencbvex  2732  gencbval  2734  sbceq2a  2919  eqimss2  3152  uneqdifeqim  3448  tppreq3  3626  copsex2t  4167  copsex2g  4168  ordsoexmid  4477  0elsucexmid  4480  ordpwsucexmid  4485  cnveqb  4994  cnveq0  4995  relcoi1  5070  funtpg  5174  f0rn0  5317  f1ocnvfv  5680  f1ocnvfvb  5681  cbvfo  5686  cbvexfo  5687  brabvv  5817  ov6g  5908  ectocld  6495  ecoptocl  6516  phplem3  6748  f1dmvrnfibi  6832  f1vrnfibi  6833  updjud  6967  pr2ne  7048  nn0ind-raph  9168  nn01to3  9409  modqmuladd  10139  modqmuladdnn0  10141  fihashf1rn  10535  hashfzp1  10570  rennim  10774  xrmaxiflemcom  11018  m1expe  11596  m1expo  11597  m1exp1  11598  nn0o1gt2  11602  flodddiv4  11631  cncongr1  11784  txcn  12444  bj-inf2vnlem2  13169