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