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

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
StepHypRef Expression
1 eqcom 2042 . 2 (𝐵 = 𝐴𝐴 = 𝐵)
2 eqcoms.1 . 2 (𝐴 = 𝐵𝜑)
31, 2sylbi 114 1 (𝐵 = 𝐴𝜑)
 Colors of variables: wff set class 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
 Copyright terms: Public domain W3C validator