Theorem eqcoms 2043

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

Syntax hints:   → wi 4   = wceq 1243

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-cleq 2033

This theorem is referenced by:  gencbvex  2600  gencbval  2602  sbceq2a  2774  eqimss2  2998  uneqdifeqim  3308  tppreq3  3473  copsex2t  3982  copsex2g  3983  ordsoexmid  4286  0elsucexmid  4289  ordpwsucexmid  4294  cnveqb  4776  cnveq0  4777  relcoi1  4849  funtpg  4950  f1ocnvfv  5419  f1ocnvfvb  5420  cbvfo  5425  cbvexfo  5426  brabvv  5551  ov6g  5638  ectocld  6172  ecoptocl  6193  phplem3  6317  nn0ind-raph  8355  nn01to3  8552  rennim  9600  bj-inf2vnlem2  10096