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

Theorem xchbinxr 324
 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 213 . 2 (𝜓𝜒)
41, 3xchbinx 323 1 (𝜑 ↔ ¬ 𝜒)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 195 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 196 This theorem is referenced by:  3anor  1047  2nalexn  1745  2exnaln  1746  sbn  2379  ralnex  2975  ralnexOLD  2976  rexanali  2981  r2exlem  3041  nss  3626  difdif  3698  difab  3855  ssdif0  3896  difin0ss  3900  sbcnel12g  3937  disjsn  4192  iundif2  4523  iindif2  4525  brsymdif  4641  notzfaus  4766  rexxfr  4814  nssss  4851  reldm0  5264  domtriord  7991  rnelfmlem  21566  dchrfi  24780  wwlknext  26252  df3nandALT2  31567  bj-ssbn  31830  poimirlem1  32580  dvasin  32666  lcvbr3  33328  cvrval2  33579  wopprc  36615  dfss6  37082  gneispace  37452  wwlksnext  41099
 Copyright terms: Public domain W3C validator