Theorem eqcoms 1478

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

Hypothesis

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

Assertion

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

Proof of Theorem eqcoms

Step	Hyp	Ref	Expression
1		eqcom 1477	. 2 |- (B = A <-> A = B)
2		eqcoms.1	. 2 |- (A = B -> ph)
3	1, 2	sylbi 199	1 |- (B = A -> ph)

Syntax hints:   -> wi 3   = wceq 956

This theorem is referenced by:  gencbvex 1838  reu8 1936  sseq1 2082  eqimss2 2110  uniiunlem 2132  copsex2g 2793  reuuni4 2887  findsg 3157  tfindsg 3162  opelxp1 3205  f1ocnvfv 3880  f1ocnvfvb 3881  oprabval6g 4032  foprab2 4119  ectocl 4302  ecoptocl 4303  phplem3 4510  indpi 5034  ltlent 5522  squeeze0 5924  nn0ind-raph 6214  sqr2irrlem1 6724  leabs 6872  efgt0 7404  reeff1o 7426  dscmet 7918  cdj1 10360  fiiu 10453  fiiuOLD 10454  oooeqim2 10476  fiiu2 10488  fiiu2OLD 10489  hmph 10524  homcard 10539  top2usne 10549  efilcp 10572  efilcpOLD 10573  efilcp2 10581  efilcp2OLD 10582  cnfilca 10583  cnfilcaOLD 10584  rcfpfillem6 10595  rcfpfillem6OLD 10596  ismona 10737  idfisf 10760

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-4 973  ax-5o 975  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1469

Copyright terms: Public domain