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

Theorem xchbinxr 334
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 223 . 2 (𝜓𝜒)
41, 3xchbinx 333 1 (𝜑 ↔ ¬ 𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205
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 206
This theorem is referenced by:  con2bii  356  2nalexn  1822  2exnaln  1823  sbn  2269  ralnex  3069  rexanali  3099  r2exlem  3140  nelbOLD  3230  dfss6  3971  nss  4046  difdif  4131  indifdi  4286  difab  4303  neq0  4349  ssdif0  4367  difin0ss  4372  sbcnel12g  4415  disjsn  4720  iundif2  5081  iindif2  5084  brsymdif  5211  rexxfr  5420  nssss  5461  reldm0  5934  domtriord  9154  rnelfmlem  23876  dchrfi  27208  noinfbnd1lem4  27679  wwlksnext  29724  dff15  34740  df3nandALT2  35917  wl-3xornot1  36992  poimirlem1  37127  dvasin  37210  lcvbr3  38527  cvrval2  38778  hashnexinj  41631  wopprc  42482  onsucf1olem  42730  sqrtcvallem1  43092  gneispace  43595  iindif2f  44561  aiota0ndef  46506
  Copyright terms: Public domain W3C validator