Theorem eqcoms 2160

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 2159	. 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 1335

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 1427  ax-gen 1429  ax-ext 2139

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

This theorem is referenced by:  gencbvex  2758  gencbval  2760  sbceq2a  2947  eqimss2  3183  uneqdifeqim  3479  tppreq3  3662  copsex2t  4204  copsex2g  4205  ordsoexmid  4519  0elsucexmid  4522  ordpwsucexmid  4527  cnveqb  5038  cnveq0  5039  relcoi1  5114  funtpg  5218  f0rn0  5361  f1ocnvfv  5724  f1ocnvfvb  5725  cbvfo  5730  cbvexfo  5731  brabvv  5861  ov6g  5952  ectocld  6539  ecoptocl  6560  phplem3  6792  f1dmvrnfibi  6881  f1vrnfibi  6882  updjud  7016  pr2ne  7110  nn0ind-raph  9264  nn01to3  9508  modqmuladd  10247  modqmuladdnn0  10249  fihashf1rn  10645  hashfzp1  10680  rennim  10884  xrmaxiflemcom  11128  m1expe  11771  m1expo  11772  m1exp1  11773  nn0o1gt2  11777  flodddiv4  11806  cncongr1  11960  txcn  12635  relogbcxpbap  13242  logbgcd1irr  13244  logbgcd1irraplemexp  13245  bj-inf2vnlem2  13505