Theorem eqcoms 2241

Description: Inference applying commutative law for class equality to an antecedent. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
eqcoms.1	⊢ (𝐴 = 𝐵 → 𝜑)

Assertion

Ref	Expression
eqcoms	⊢ (𝐵 = 𝐴 → 𝜑)

Proof of Theorem eqcoms

Step	Hyp	Ref	Expression
1		eqcom 2240	. 2 ⊢ (𝐵 = 𝐴 ↔ 𝐴 = 𝐵)
2		eqcoms.1	. 2 ⊢ (𝐴 = 𝐵 → 𝜑)
3	1, 2	sylbi 121	1 ⊢ (𝐵 = 𝐴 → 𝜑)

This proof depends on syntax axioms:   → wi 4   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  gencbvex  2869  gencbval  2871  sbceq2a  3062  eqimss2  3303  uneqdifeqim  3613  tppreq3  3814  ifpprsnssdc  3820  copsex2t  4387  copsex2g  4388  ordsoexmid  4711  0elsucexmid  4714  ordpwsucexmid  4719  cnveqb  5246  cnveq0  5247  relcoi1  5322  funtpg  5435  f0rn0  5590  fimadmfo  5627  f1ssf1  5674  f1ocnvfv  5988  f1ocnvfvb  5989  cbvfo  5994  cbvexfo  5995  riotaeqimp  6066  brabvv  6137  ov6g  6230  ectocld  6879  ecoptocl  6900  phplem3  7160  f1dmvrnfibi  7263  f1vrnfibi  7264  updjud  7429  pr2ne  7545  nn0ind-raph  9775  nn01to3  10034  modqmuladd  10825  modqmuladdnn0  10827  fihashf1rn  11250  hashfzp1  11288  lswlgt0cl  11380  wrd2ind  11518  pfxccatin12lem2  11526  pfxccatin12lem3  11527  rennim  11791  xrmaxiflemcom  12041  m1expe  12692  m1expo  12693  m1exp1  12694  nn0o1gt2  12698  flodddiv4  12729  cncongr1  12907  m1dvdsndvds  13057  mgmsscl  13741  mndinvmod  13818  ringinvnzdiv  14463  txcn  15513  relogbcxpbap  16213  logbgcd1irr  16215  logbgcd1irraplemexp  16216  fsumdvdsmul  16297  zabsle1  16335  2lgslem1c  16426  2lgsoddprmlem3  16447  upgrpredgv  16604  usgredg2vlem2  16681  ushgredgedg  16684  ushgredgedgloop  16686  ifpsnprss  16801  upgrwlkvtxedg  16822  uspgr2wlkeq  16823  eupth2lem3lem3fi  16928  eupth2lem3lem4fi  16931  bj-inf2vnlem2  17214