Theorem eqcoms 2199

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 2198	. 2 ⊢ (𝐵 = 𝐴 ↔ 𝐴 = 𝐵)
2		eqcoms.1	. 2 ⊢ (𝐴 = 𝐵 → 𝜑)
3	1, 2	sylbi 121	1 ⊢ (𝐵 = 𝐴 → 𝜑)

Syntax hints:   → wi 4   = wceq 1364

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 1461  ax-gen 1463  ax-ext 2178

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

This theorem is referenced by:  gencbvex  2810  gencbval  2812  sbceq2a  3000  eqimss2  3239  uneqdifeqim  3537  tppreq3  3726  copsex2t  4279  copsex2g  4280  ordsoexmid  4599  0elsucexmid  4602  ordpwsucexmid  4607  cnveqb  5126  cnveq0  5127  relcoi1  5202  funtpg  5310  f0rn0  5455  fimadmfo  5492  f1ocnvfv  5829  f1ocnvfvb  5830  cbvfo  5835  cbvexfo  5836  brabvv  5972  ov6g  6065  ectocld  6669  ecoptocl  6690  phplem3  6924  f1dmvrnfibi  7019  f1vrnfibi  7020  updjud  7157  pr2ne  7273  nn0ind-raph  9462  nn01to3  9710  modqmuladd  10477  modqmuladdnn0  10479  fihashf1rn  10899  hashfzp1  10935  rennim  11186  xrmaxiflemcom  11433  m1expe  12083  m1expo  12084  m1exp1  12085  nn0o1gt2  12089  flodddiv4  12120  cncongr1  12298  m1dvdsndvds  12444  mgmsscl  13065  mndinvmod  13149  ringinvnzdiv  13684  txcn  14597  relogbcxpbap  15287  logbgcd1irr  15289  logbgcd1irraplemexp  15290  fsumdvdsmul  15313  zabsle1  15326  2lgslem1c  15417  2lgsoddprmlem3  15438  bj-inf2vnlem2  15703