Theorem eqcoms 2235

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 2234	. 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 1398

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 1496  ax-gen 1498  ax-ext 2214

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

This theorem is referenced by:  gencbvex  2861  gencbval  2863  sbceq2a  3053  eqimss2  3293  uneqdifeqim  3595  tppreq3  3794  ifpprsnssdc  3799  copsex2t  4361  copsex2g  4362  ordsoexmid  4684  0elsucexmid  4687  ordpwsucexmid  4692  cnveqb  5218  cnveq0  5219  relcoi1  5294  funtpg  5407  f0rn0  5562  fimadmfo  5599  f1ssf1  5646  f1ocnvfv  5952  f1ocnvfvb  5953  cbvfo  5958  cbvexfo  5959  riotaeqimp  6028  brabvv  6099  ov6g  6192  ectocld  6835  ecoptocl  6856  phplem3  7108  f1dmvrnfibi  7211  f1vrnfibi  7212  updjud  7373  pr2ne  7489  nn0ind-raph  9695  nn01to3  9949  modqmuladd  10728  modqmuladdnn0  10730  fihashf1rn  11151  hashfzp1  11189  lswlgt0cl  11277  wrd2ind  11415  pfxccatin12lem2  11423  pfxccatin12lem3  11424  rennim  11687  xrmaxiflemcom  11934  m1expe  12585  m1expo  12586  m1exp1  12587  nn0o1gt2  12591  flodddiv4  12622  cncongr1  12800  m1dvdsndvds  12946  mgmsscl  13574  mndinvmod  13658  ringinvnzdiv  14194  txcn  15140  relogbcxpbap  15830  logbgcd1irr  15832  logbgcd1irraplemexp  15833  fsumdvdsmul  15859  zabsle1  15872  2lgslem1c  15963  2lgsoddprmlem3  15984  upgrpredgv  16141  usgredg2vlem2  16218  ushgredgedg  16221  ushgredgedgloop  16223  ifpsnprss  16338  upgrwlkvtxedg  16359  uspgr2wlkeq  16360  eupth2lem3lem3fi  16465  eupth2lem3lem4fi  16468  bj-inf2vnlem2  16741