Theorem eqcoms 2180

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

Syntax hints:   -> wi 4   = wceq 1353

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170

This theorem is referenced by:  gencbvex  2785  gencbval  2787  sbceq2a  2975  eqimss2  3212  uneqdifeqim  3510  tppreq3  3697  copsex2t  4247  copsex2g  4248  ordsoexmid  4563  0elsucexmid  4566  ordpwsucexmid  4571  cnveqb  5086  cnveq0  5087  relcoi1  5162  funtpg  5269  f0rn0  5412  f1ocnvfv  5782  f1ocnvfvb  5783  cbvfo  5788  cbvexfo  5789  brabvv  5923  ov6g  6014  ectocld  6603  ecoptocl  6624  phplem3  6856  f1dmvrnfibi  6945  f1vrnfibi  6946  updjud  7083  pr2ne  7193  nn0ind-raph  9372  nn01to3  9619  modqmuladd  10368  modqmuladdnn0  10370  fihashf1rn  10770  hashfzp1  10806  rennim  11013  xrmaxiflemcom  11259  m1expe  11906  m1expo  11907  m1exp1  11908  nn0o1gt2  11912  flodddiv4  11941  cncongr1  12105  m1dvdsndvds  12250  mgmsscl  12785  mndinvmod  12851  ringinvnzdiv  13232  txcn  13814  relogbcxpbap  14422  logbgcd1irr  14424  logbgcd1irraplemexp  14425  zabsle1  14439  2lgsoddprmlem3  14498  bj-inf2vnlem2  14762