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

Theorem xchbinxr 327
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 216 . 2 (𝜓𝜒)
41, 3xchbinx 326 1 (𝜑 ↔ ¬ 𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 198
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 199
This theorem is referenced by:  2nalexn  1871  2exnaln  1872  sbn  2467  ralnex  3174  rexanali  3179  r2exlem  3244  dfss6  3811  nss  3882  difdif  3959  difab  4122  ssdif0  4172  difin0ss  4177  sbcnel12g  4210  disjsn  4478  iundif2  4822  iindif2  4824  brsymdif  4947  notzfaus  5076  rexxfr  5130  nssss  5158  reldm0  5590  domtriord  8396  rnelfmlem  22175  dchrfi  25443  wwlksnext  27271  df3nandALT2  32991  bj-ssbn  33239  poimirlem1  34045  dvasin  34130  lcvbr3  35186  cvrval2  35437  wopprc  38570  gneispace  39402  aiota0ndef  42139
  Copyright terms: Public domain W3C validator