ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eqcomi Structured version   GIF version

Theorem eqcomi 2026
Description: Inference from commutative law for class equality. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
eqcomi.1 A = B
Assertion
Ref Expression
eqcomi B = A

Proof of Theorem eqcomi
StepHypRef Expression
1 eqcomi.1 . 2 A = B
2 eqcom 2024 . 2 (A = BB = A)
31, 2mpbi 133 1 B = A
Colors of variables: wff set class
Syntax hints:   = wceq 1228
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 1316  ax-gen 1318  ax-ext 2004
This theorem depends on definitions:  df-bi 110  df-cleq 2015
This theorem is referenced by:  eqtr2i  2043  eqtr3i  2044  eqtr4i  2045  syl5eqr  2068  syl5reqr  2069  syl6eqr  2072  syl6reqr  2073  eqeltrri  2093  eleqtrri  2095  syl5eqelr  2107  syl6eleqr  2113  abid2  2140  abid2f  2184  eqnetrri  2208  neeqtrri  2212  eqsstr3i  2953  sseqtr4i  2955  syl5eqssr  2967  syl6sseqr  2969  difdif2ss  3171  inrab2  3187  dfopg  3521  opid  3541  eqbrtrri  3759  breqtrri  3763  syl6breqr  3778  pwin  3993  limon  4188  tfis  4233  dfdm2  4779  cnvresid  4899  fores  5040  funcoeqres  5082  f1oprg  5093  fmptpr  5280  fsnunres  5289  riotaprop  5415  fo1st  5707  fo2nd  5708  ax0id  6572  bdceqir  7071  bj-ssom  7158
  Copyright terms: Public domain W3C validator