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

Theorem xchbinxr 338
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 227 . 2 (𝜓𝜒)
41, 3xchbinx 337 1 (𝜑 ↔ ¬ 𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 209
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 210
This theorem is referenced by:  con2bii  361  2nalexn  1835  2exnaln  1836  sbn  2282  ralnex  3162  rexanali  3190  nelbOLD  3194  r2exlem  3229  dfss6  3903  nss  3977  difdif  4059  indifdi  4212  difab  4229  neq0  4274  ssdif0  4292  difin0ss  4297  sbcnel12g  4340  disjsn  4641  iundif2  4996  iindif2  4999  brsymdif  5126  notzfausOLD  5269  rexxfr  5323  nssss  5354  reldm0  5811  domtriord  8814  rnelfmlem  22873  dchrfi  26160  wwlksnext  28001  dff15  32792  noinfbnd1lem4  33692  df3nandALT2  34352  wl-3xornot1  35414  poimirlem1  35541  dvasin  35624  lcvbr3  36800  cvrval2  37051  wopprc  40583  sqrtcvallem1  40943  gneispace  41449  aiota0ndef  44289
  Copyright terms: Public domain W3C validator