Theorem eqcoms 2196

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 2195	. 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 1458  ax-gen 1460  ax-ext 2175

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

This theorem is referenced by:  gencbvex  2807  gencbval  2809  sbceq2a  2997  eqimss2  3235  uneqdifeqim  3533  tppreq3  3722  copsex2t  4275  copsex2g  4276  ordsoexmid  4595  0elsucexmid  4598  ordpwsucexmid  4603  cnveqb  5122  cnveq0  5123  relcoi1  5198  funtpg  5306  f0rn0  5449  fimadmfo  5486  f1ocnvfv  5823  f1ocnvfvb  5824  cbvfo  5829  cbvexfo  5830  brabvv  5965  ov6g  6058  ectocld  6657  ecoptocl  6678  phplem3  6912  f1dmvrnfibi  7005  f1vrnfibi  7006  updjud  7143  pr2ne  7254  nn0ind-raph  9437  nn01to3  9685  modqmuladd  10440  modqmuladdnn0  10442  fihashf1rn  10862  hashfzp1  10898  rennim  11149  xrmaxiflemcom  11395  m1expe  12043  m1expo  12044  m1exp1  12045  nn0o1gt2  12049  flodddiv4  12078  cncongr1  12244  m1dvdsndvds  12389  mgmsscl  12947  mndinvmod  13029  ringinvnzdiv  13549  txcn  14454  relogbcxpbap  15138  logbgcd1irr  15140  logbgcd1irraplemexp  15141  zabsle1  15156  2lgslem1c  15247  2lgsoddprmlem3  15268  bj-inf2vnlem2  15533