Theorem negbii 187

Description: Negate both sides of a logical equivalence.

Hypothesis

Ref	Expression
bi.a	⊢ (φ ↔ ψ)

Assertion

Ref	Expression
negbii	⊢ (¬ φ ↔ ¬ ψ)

Proof of Theorem negbii

Step	Hyp	Ref	Expression
1		bi.a	. . . 4 ⊢ (φ ↔ ψ)
2	1	biimpr 152	. . 3 ⊢ (ψ → φ)
3	2	con3i 98	. 2 ⊢ (¬ φ → ¬ ψ)
4	1	biimp 151	. . 3 ⊢ (φ → ψ)
5	4	con3i 98	. 2 ⊢ (¬ ψ → ¬ φ)
6	3, 5	impbi 157	1 ⊢ (¬ φ ↔ ¬ ψ)

Syntax hints:  ¬ wn 2   ↔ wb 146

This theorem is referenced by:  mtbi 191  mtbir 192  anor 304  ianor 305  ioran 306  pm4.52 307  pm4.54 309  oran 312  anass 441  andi 606  pm5.18 662  pm5.24 674  oplem1 774  19.43 1090  cbvex 1168  sban 1239  sb8e 1264  sbex 1350  necon3abii 1599  ralnex 1656  rexnal 1657  nss 2116  dfpss3 2137  difdif 2169  nssinpss 2243  nsspssun 2244  dfss4 2245  difin 2248  difab 2272  reuun2 2281  ne0f 2291  ssdif0 2331  ssnelpss 2334  difin0ss 2336  inssdif0 2337  rexpr 2433  iundif2 2615  iindif2 2616  notzfaus 2746  nssss 2770  dtru 2778  pwundif 2834  rexxfr 2907  dffr2 2925  efrirr 2934  efrn2lp 2935  epne3 2936  dfwe2 2941  ordtri3or 2985  rexxp 3225  dm0rn0 3336  reldm0 3337  imadif 3580  fn0 3611  tz6.12-2 3745  rdgsucopabn 3953  tz7.48lem 3961  ndmoprcom 4053  1st2val 4101  2nd2val 4102  0nelqs 4304  brsdom 4387  brsdom2 4467  php3 4521  php3OLD 4522  suc11reg 4614  inf3lem6 4627  r1tr 4664  ranklim 4695  rankuni 4708  rankxplim2 4723  rankxplim3 4724  rankxpsuc 4725  kmlem4 4778  zorn 4807  alephon 4876  alephcard 4878  alephnbtwn 4879  alephval3 4914  cfub 4920  cardcf 4923  cflecard 4924  cfle 4925  psslinpr 5147  ltsor 5273  axrrecex 5296  leadd1 5604  dfinfmr 6069  infmsup 6070  arch 6073  infmxrcl 6088  fzneuzt 6519  crne0 6740  dfisum 7191  isumshft 7204  isumshft2 7205  reef11 7408  infxpidmlem8 7560  alephadd 7584  fctopOLD 7647  cctop 7649  clsval2 7682  ntreq0 7705  spwnex3 8651  cosh111lem3 8711  efif1lem5 8729  efif1lem7 8731  avril1 8779  shne0 9366  chnle 9403  nonbool 9591  lnfncon 9985  strlem1 10172  cvbr2t 10205  cvnbtwn2t 10209  cvnbtwn3t 10210  cvnbtwn4t 10211  hatomistic 10284  chrelat2 10287  atabs2 10324  dmdbr5at 10344  intn3an1d 10423  intn3an2d 10424  intn3an3d 10425  cdrci 10480  efilcp 10556  efilcp2 10561  cnfilca 10562

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147

Copyright terms: Public domain