Theorem eqcoms 2173

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 2172	. 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 1348

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 1440  ax-gen 1442  ax-ext 2152

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

This theorem is referenced by:  gencbvex  2776  gencbval  2778  sbceq2a  2965  eqimss2  3202  uneqdifeqim  3500  tppreq3  3686  copsex2t  4230  copsex2g  4231  ordsoexmid  4546  0elsucexmid  4549  ordpwsucexmid  4554  cnveqb  5066  cnveq0  5067  relcoi1  5142  funtpg  5249  f0rn0  5392  f1ocnvfv  5758  f1ocnvfvb  5759  cbvfo  5764  cbvexfo  5765  brabvv  5899  ov6g  5990  ectocld  6579  ecoptocl  6600  phplem3  6832  f1dmvrnfibi  6921  f1vrnfibi  6922  updjud  7059  pr2ne  7169  nn0ind-raph  9329  nn01to3  9576  modqmuladd  10322  modqmuladdnn0  10324  fihashf1rn  10723  hashfzp1  10759  rennim  10966  xrmaxiflemcom  11212  m1expe  11858  m1expo  11859  m1exp1  11860  nn0o1gt2  11864  flodddiv4  11893  cncongr1  12057  m1dvdsndvds  12202  mgmsscl  12615  mndinvmod  12678  txcn  13069  relogbcxpbap  13677  logbgcd1irr  13679  logbgcd1irraplemexp  13680  zabsle1  13694  bj-inf2vnlem2  14006