NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  eqcoms GIF version

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
StepHypRef Expression
1 eqcom 2355 . 2 (B = AA = B)
2 eqcoms.1 . 2 (A = Bφ)
31, 2sylbi 187 1 (B = Aφ)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1642
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-ext 2334
This theorem depends on definitions:  df-bi 177  df-cleq 2346
This theorem is referenced by:  gencbvex  2901  sbceq2a  3057  sbcco2  3069  eqimss2  3324  uneqdifeq  3638  iotaval  4350  nnsucelr  4428  phi11  4596  phi011  4599  copsex2t  4608  copsex2g  4609  f1ocnvfv  5478  f1ocnvfvb  5479  ov6g  5600  ectocld  5991  ecoptocl  5996  enprmaplem5  6080  ncelncs  6120  1cnc  6139  ncslesuc  6267
  Copyright terms: Public domain W3C validator