Theorem eqcoms 2168

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

Syntax hints:   → wi 4   = wceq 1343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158

This theorem is referenced by:  gencbvex  2772  gencbval  2774  sbceq2a  2961  eqimss2  3197  uneqdifeqim  3494  tppreq3  3679  copsex2t  4223  copsex2g  4224  ordsoexmid  4539  0elsucexmid  4542  ordpwsucexmid  4547  cnveqb  5059  cnveq0  5060  relcoi1  5135  funtpg  5239  f0rn0  5382  f1ocnvfv  5747  f1ocnvfvb  5748  cbvfo  5753  cbvexfo  5754  brabvv  5888  ov6g  5979  ectocld  6567  ecoptocl  6588  phplem3  6820  f1dmvrnfibi  6909  f1vrnfibi  6910  updjud  7047  pr2ne  7148  nn0ind-raph  9308  nn01to3  9555  modqmuladd  10301  modqmuladdnn0  10303  fihashf1rn  10702  hashfzp1  10737  rennim  10944  xrmaxiflemcom  11190  m1expe  11836  m1expo  11837  m1exp1  11838  nn0o1gt2  11842  flodddiv4  11871  cncongr1  12035  m1dvdsndvds  12180  mgmsscl  12592  txcn  12915  relogbcxpbap  13523  logbgcd1irr  13525  logbgcd1irraplemexp  13526  zabsle1  13540  bj-inf2vnlem2  13853