Theorem eqcoms 2143

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 2142	. 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 1332

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 1424  ax-gen 1426  ax-ext 2122

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

This theorem is referenced by:  gencbvex  2735  gencbval  2737  sbceq2a  2923  eqimss2  3157  uneqdifeqim  3453  tppreq3  3634  copsex2t  4175  copsex2g  4176  ordsoexmid  4485  0elsucexmid  4488  ordpwsucexmid  4493  cnveqb  5002  cnveq0  5003  relcoi1  5078  funtpg  5182  f0rn0  5325  f1ocnvfv  5688  f1ocnvfvb  5689  cbvfo  5694  cbvexfo  5695  brabvv  5825  ov6g  5916  ectocld  6503  ecoptocl  6524  phplem3  6756  f1dmvrnfibi  6840  f1vrnfibi  6841  updjud  6975  pr2ne  7065  nn0ind-raph  9192  nn01to3  9436  modqmuladd  10170  modqmuladdnn0  10172  fihashf1rn  10567  hashfzp1  10602  rennim  10806  xrmaxiflemcom  11050  m1expe  11632  m1expo  11633  m1exp1  11634  nn0o1gt2  11638  flodddiv4  11667  cncongr1  11820  txcn  12483  relogbcxpbap  13090  logbgcd1irr  13092  logbgcd1irraplemexp  13093  bj-inf2vnlem2  13340