Theorem eqcoms 2356

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

Hypothesis

Ref	Expression
eqcoms.1	⊢ (A = B → φ)

Assertion

Ref	Expression
eqcoms	⊢ (B = A → φ)

Proof of Theorem eqcoms

Step	Hyp	Ref	Expression
1		eqcom 2355	. 2 ⊢ (B = A ↔ A = B)
2		eqcoms.1	. 2 ⊢ (A = B → φ)
3	1, 2	sylbi 187	1 ⊢ (B = A → φ)

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-ext 2334

This proof depends on definitions:  df-bi 177  df-cleq 2346

This theorem is used by:  gencbvex  2902  sbceq2a  3058  sbcco2  3070  eqimss2  3325  uneqdifeq  3639  iotaval  4351  nnsucelr  4429  phi11  4597  phi011  4600  copsex2t  4609  copsex2g  4610  f1ocnvfv  5479  f1ocnvfvb  5480  ov6g  5601  ectocld  5992  ecoptocl  5997  enprmaplem5  6081  ncelncs  6121  1cnc  6140  ncslesuc  6268