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 ⊢ (𝐵 = 𝐴 → 𝜑)

Syntax hints:   → wi 4   = wceq 1402

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 1500  ax-gen 1502  ax-ext 2220

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

This theorem is referenced by:  gencbvex  2869  gencbval  2871  sbceq2a  3062  eqimss2  3303  uneqdifeqim  3613  tppreq3  3813  ifpprsnssdc  3818  copsex2t  4383  copsex2g  4384  ordsoexmid  4707  0elsucexmid  4710  ordpwsucexmid  4715  cnveqb  5241  cnveq0  5242  relcoi1  5317  funtpg  5430  f0rn0  5585  fimadmfo  5622  f1ssf1  5669  f1ocnvfv  5979  f1ocnvfvb  5980  cbvfo  5985  cbvexfo  5986  riotaeqimp  6057  brabvv  6128  ov6g  6221  ectocld  6869  ecoptocl  6890  phplem3  7149  f1dmvrnfibi  7252  f1vrnfibi  7253  updjud  7416  pr2ne  7532  nn0ind-raph  9746  nn01to3  10000  modqmuladd  10786  modqmuladdnn0  10788  fihashf1rn  11210  hashfzp1  11248  lswlgt0cl  11340  wrd2ind  11478  pfxccatin12lem2  11486  pfxccatin12lem3  11487  rennim  11751  xrmaxiflemcom  11998  m1expe  12649  m1expo  12650  m1exp1  12651  nn0o1gt2  12655  flodddiv4  12686  cncongr1  12864  m1dvdsndvds  13010  mgmsscl  13664  mndinvmod  13741  ringinvnzdiv  14338  txcn  15359  relogbcxpbap  16050  logbgcd1irr  16052  logbgcd1irraplemexp  16053  fsumdvdsmul  16088  zabsle1  16101  2lgslem1c  16192  2lgsoddprmlem3  16213  upgrpredgv  16370  usgredg2vlem2  16447  ushgredgedg  16450  ushgredgedgloop  16452  ifpsnprss  16567  upgrwlkvtxedg  16588  uspgr2wlkeq  16589  eupth2lem3lem3fi  16694  eupth2lem3lem4fi  16697  bj-inf2vnlem2  16980