Theorem eqcoms 2232

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 2231	. 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 1395

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 1493  ax-gen 1495  ax-ext 2211

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

This theorem is referenced by:  gencbvex  2848  gencbval  2850  sbceq2a  3040  eqimss2  3280  uneqdifeqim  3578  tppreq3  3772  ifpprsnssdc  3777  copsex2t  4335  copsex2g  4336  ordsoexmid  4658  0elsucexmid  4661  ordpwsucexmid  4666  cnveqb  5190  cnveq0  5191  relcoi1  5266  funtpg  5378  f0rn0  5528  fimadmfo  5565  f1ocnvfv  5915  f1ocnvfvb  5916  cbvfo  5921  cbvexfo  5922  riotaeqimp  5991  brabvv  6062  ov6g  6155  ectocld  6765  ecoptocl  6786  phplem3  7035  f1dmvrnfibi  7134  f1vrnfibi  7135  updjud  7272  pr2ne  7388  nn0ind-raph  9587  nn01to3  9841  modqmuladd  10618  modqmuladdnn0  10620  fihashf1rn  11040  hashfzp1  11078  lswlgt0cl  11156  wrd2ind  11294  pfxccatin12lem2  11302  pfxccatin12lem3  11303  rennim  11553  xrmaxiflemcom  11800  m1expe  12450  m1expo  12451  m1exp1  12452  nn0o1gt2  12456  flodddiv4  12487  cncongr1  12665  m1dvdsndvds  12811  mgmsscl  13434  mndinvmod  13518  ringinvnzdiv  14053  txcn  14989  relogbcxpbap  15679  logbgcd1irr  15681  logbgcd1irraplemexp  15682  fsumdvdsmul  15705  zabsle1  15718  2lgslem1c  15809  2lgsoddprmlem3  15830  upgrpredgv  15985  usgredg2vlem2  16062  ushgredgedg  16065  ushgredgedgloop  16067  ifpsnprss  16140  upgrwlkvtxedg  16161  uspgr2wlkeq  16162  bj-inf2vnlem2  16502