Theorem eqcoms 2091

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

Syntax hints:   -> wi 4   = wceq 1289

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-ext 2070

This theorem depends on definitions:  df-bi 115  df-cleq 2081

This theorem is referenced by:  gencbvex  2665  gencbval  2667  sbceq2a  2850  eqimss2  3079  uneqdifeqim  3368  tppreq3  3545  copsex2t  4072  copsex2g  4073  ordsoexmid  4378  0elsucexmid  4381  ordpwsucexmid  4386  cnveqb  4886  cnveq0  4887  relcoi1  4962  funtpg  5065  f0rn0  5205  f1ocnvfv  5558  f1ocnvfvb  5559  cbvfo  5564  cbvexfo  5565  brabvv  5695  ov6g  5782  ectocld  6356  ecoptocl  6377  phplem3  6568  f1dmvrnfibi  6651  f1vrnfibi  6652  updjud  6771  pr2ne  6818  nn0ind-raph  8861  nn01to3  9100  modqmuladd  9769  modqmuladdnn0  9771  fihashf1rn  10193  hashfzp1  10228  rennim  10431  m1expe  11173  m1expo  11174  m1exp1  11175  nn0o1gt2  11179  flodddiv4  11208  cncongr1  11359  bj-inf2vnlem2  11821