MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xchbinxr Structured version   Visualization version   GIF version

Theorem xchbinxr 324
Description: Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.)
Hypotheses
Ref Expression
xchbinxr.1 (𝜑 ↔ ¬ 𝜓)
xchbinxr.2 (𝜒𝜓)
Assertion
Ref Expression
xchbinxr (𝜑 ↔ ¬ 𝜒)

Proof of Theorem xchbinxr
StepHypRef Expression
1 xchbinxr.1 . 2 (𝜑 ↔ ¬ 𝜓)
2 xchbinxr.2 . . 3 (𝜒𝜓)
32bicomi 214 . 2 (𝜓𝜒)
41, 3xchbinx 323 1 (𝜑 ↔ ¬ 𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 197
This theorem is referenced by:  3anorOLD  1094  2nalexn  1892  2exnaln  1893  sbn  2516  ralnex  3118  ralnexOLD  3119  rexanali  3124  r2exlem  3185  dfss6  3722  nss  3792  difdif  3867  difab  4027  ssdif0  4073  difin0ss  4077  sbcnel12g  4116  disjsn  4378  iundif2  4727  iindif2  4729  brsymdif  4851  notzfaus  4977  rexxfr  5025  nssss  5061  reldm0  5486  domtriord  8259  rnelfmlem  21928  dchrfi  25150  wwlksnext  26982  df3nandALT2  32674  bj-ssbn  32918  poimirlem1  33692  dvasin  33778  lcvbr3  34782  cvrval2  35033  wopprc  38068  gneispace  38903
  Copyright terms: Public domain W3C validator