Theorem cleqcoms 1104

Description: Inference applying commutative law for class equality to an antecedent.

Hypothesis

Ref	Expression
cleqcoms.1	|- (A = B -> ph)

Assertion

Ref	Expression
cleqcoms	|- (B = A -> ph)

Proof of Theorem cleqcoms

Step	Hyp	Ref	Expression
1		cleqcom 1103	. 2 |- (B = A <-> A = B)
2		cleqcoms.1	. 2 |- (A = B -> ph)
3	1, 2	sylbi 174	1 |- (B = A -> ph)

Syntax hints:   -> wi 2   = wceq 1091

This theorem is referenced by:  gencbvex 1372  sseq1 1521  eqimss2 1549  copsex2g 1903  reuuni4 1959  findsg 2398  tfindsg 2402  f1oco 2816  f1ocnvfv 2921  f1ocnvfvb 2922  oprabval4g 3053  ectocl 3238  ecoptocl 3239  phplem4 3406  indpi 3828  nn0ind 4612  sqr2irrlem1 4777  leabs 4852

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-cleq 1097

metamath.org