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

Theorem xchbinxr 323
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 212 . 2 (𝜓𝜒)
41, 3xchbinx 322 1 (𝜑 ↔ ¬ 𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 194
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 195
This theorem is referenced by:  3anor  1046  2nalexn  1744  2exnaln  1745  sbn  2378  ralnex  2974  ralnexOLD  2975  rexanali  2980  r2exlem  3040  nss  3625  difdif  3697  difab  3854  ssdif0  3895  difin0ss  3899  sbcnel12g  3936  disjsn  4191  iundif2  4517  iindif2  4519  brsymdif  4635  notzfaus  4761  rexxfr  4809  nssss  4845  reldm0  5251  domtriord  7968  rnelfmlem  21508  dchrfi  24697  wwlknext  26018  df3nandALT2  31373  bj-ssbn  31636  poimirlem1  32376  dvasin  32462  lcvbr3  33124  cvrval2  33375  wopprc  36411  dfss6  36878  gneispace  37248  wwlksnext  41094
  Copyright terms: Public domain W3C validator