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

Theorem xchbinxr 337
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 226 . 2 (𝜓𝜒)
41, 3xchbinx 336 1 (𝜑 ↔ ¬ 𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 208
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 209
This theorem is referenced by:  con2bii  360  2nalexn  1828  2exnaln  1829  sbn  2287  sbnOLD  2541  sbnALT  2595  ralnex  3223  rexanali  3252  nelb  3255  r2exlem  3289  dfss6  3936  nss  4008  difdif  4086  difab  4250  ssdif0  4299  difin0ss  4304  sbcnel12g  4339  disjsn  4623  iundif2  4972  iindif2  4975  brsymdif  5101  notzfausOLD  5239  rexxfr  5293  nssss  5324  reldm0  5774  domtriord  8641  rnelfmlem  22536  dchrfi  25818  wwlksnext  27658  dff15  32361  df3nandALT2  33756  wl-3xornot1  34774  poimirlem1  34934  dvasin  35017  lcvbr3  36195  cvrval2  36446  wopprc  39764  gneispace  40619  aiota0ndef  43443
  Copyright terms: Public domain W3C validator