Theorem eqcoms 2084

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 2083	. 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 1284

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 1376  ax-gen 1378  ax-ext 2063

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

This theorem is referenced by:  gencbvex  2645  gencbval  2647  sbceq2a  2825  eqimss2  3052  uneqdifeqim  3328  tppreq3  3495  copsex2t  4000  copsex2g  4001  ordsoexmid  4305  0elsucexmid  4308  ordpwsucexmid  4313  cnveqb  4796  cnveq0  4797  relcoi1  4869  funtpg  4970  f1ocnvfv  5439  f1ocnvfvb  5440  cbvfo  5445  cbvexfo  5446  brabvv  5571  ov6g  5658  ectocld  6195  ecoptocl  6216  phplem3  6340  f1dmvrnfibi  6393  f1vrnfibi  6394  pr2ne  6461  nn0ind-raph  8464  nn01to3  8702  modqmuladd  9368  modqmuladdnn0  9370  rennim  9888  m1expe  10299  m1expo  10300  m1exp1  10301  nn0o1gt2  10305  flodddiv4  10334  cncongr1  10485  bj-inf2vnlem2  10766