Theorem notbii 300

Description: Negate both sides of a logical equivalence.

Hypothesis

Ref	Expression
bi.a	|- (ph <-> ps)

Assertion

Ref	Expression
notbii	|- (-. ph <-> -. ps)

Proof of Theorem notbii

Step	Hyp	Ref	Expression
1		bi.a	. . . 4 |- (ph <-> ps)
2	1	biimpri 230	. . 3 |- (ps -> ph)
3	2	con3i 149	. 2 |- (-. ph -> -. ps)
4	1	biimpi 224	. . 3 |- (ph -> ps)
5	4	con3i 149	. 2 |- (-. ps -> -. ph)
6	3, 5	impbii 223	1 |- (-. ph <-> -. ps)

Syntax hints:  -. wn 2   <-> wb 219

This theorem is referenced by:  mtbiOLD 313  mtbirOLD 315  con1bii 333  anorOLD 422  ioran 424  pm4.52 425  pm4.54 427  pm4.52OLD 480  pm4.54OLD 481  anassOLD 634  andiOLD 944  pm5.18OLD 984  pm5.24 995  xordi 997  oplem1 1095  oplem1OLD 1096  3anor 1113  3ioran 1115  nic-justlem 1506  nic-justneg 1508  nic-justbi 1509  nic-mpALT 1513  nic-axALT 1515  19.43 1725  cbvex 1809  sban 1883  sb8e 1909  sbex 2003  necon3abii 2295  ralnex 2363  rexnal 2364  nss 2898  difdif 2953  nsspssun 3037  dfss4 3038  indifdir 3059  undif3 3063  difab 3071  reuun2 3080  n0f 3090  ssdif0 3135  ssnelpss 3138  difin0ss 3140  inssdif0 3141  rexpr 3273  disjsn 3280  difprsn 3321  iundif2 3492  iindif2 3494  brdif 3560  notzfaus 3646  nssss 3673  dtruALT 3680  pwundif 3740  posn 3762  pofun 3763  efrirr 3793  efrn2lp 3794  ordtri3or 3843  rexxfr 3987  epne3 4006  tfinds 4079  rexxp 4175  rexxpf 4177  dm0rn0 4298  reldm0 4299  intirr 4425  imadif 4593  tz6.12-2 4785  dffv2 4820  ndmoprcom 5073  1st2val 5144  2nd2val 5145  frxp 5210  poxp 5212  iotanul 5232  rdgsucopabn 5319  tz7.48lem 5328  brsdom 5601  brsdom2 5690  domtriord 5713  riotav 5734  riotaprc 5736  php3 5801  unxpdomlem2 5818  unxpdomlem3 5819  fimax 5846  wofi 5850  dfsup2 5889  dfsup2OLD 5890  ordiso 5914  ordtypelem7 5921  suc11reg 5942  inf3lem6 5956  zfregs2 5991  r1tr 6001  ranklim 6032  rankuni 6045  rankxplim2 6060  rankxplim3 6061  rankxpsuc 6062  alephon 6154  alephcard 6156  alephnbtwn 6157  mappwen 6182  alephval3 6233  onacda 6259  cfub 6268  cardcf 6271  cflecard 6272  cfle 6273  cfsuc 6276  cflim2 6283  cfidm 6290  domtriom 6297  domtriomOLD 6299  axcclem 6312  kmlem4 6340  zorn 6370  alephcardOLD 6431  alephnbtwnOLD 6432  alephreg 6449  pwcfsdom 6450  cfpwsdom 6451  psslinpr 6653  ltsor 6779  axrrecex 6800  leadd1i 7121  rpneg 7592  dfinfmr 7616  infmsup 7617  arch 7620  infmxrcl 7635  difreicc 7932  fzneuz 8068  crne0i 8373  dfisum 8848  isumshfti 8861  isumshft2i 8862  reef11i 9071  infxpidmlem8OLD 9222  alephadd 9245  gcd0id 9323  mulgcdlem2 9352  isprm2lem 9368  fctop 9771  cctop 9773  clsval2 9825  ntreq0 9848  spwnex3 10869  cosh111lem3 10941  efif1lem5 10959  efif1lem7 10961  avril1 11013  fbunfip 11120  extbas1 11129  filrn 11131  shne0i 11838  chnlei 11875  nonbooli 12063  lnfnconi 12459  strlem1 12653  cvbr2 12686  cvnbtwn2 12690  cvnbtwn3 12691  cvnbtwn4 12692  hatomistici 12765  chrelat2i 12768  atabs2i 12805  dmdbr5ati 12825  bnj8 13174  bnj11 13177  bnj24 13187  bnj29 13192  bnj112 13239  bnj1144 13712  bnj1164 13727  bnj1215 13762  bnj1222 13766  bnj1391 13876  bnj1392 13877  bnj1393 13878  bnj1394 13879  bnj1476 13927  bnj1533 13953  bnj1174 14213  bnj1284 14253  efrunt 14432  indifdiOLD 14453  dftr6 14460  fundmpss 14467  dfon2lem4 14486  dfon2lem5 14487  dfon2lem7 14489  dfon2lem8 14490  dfon2lem9 14491  omopthi 14503  frsucopabn 14554  poxpOLD 14602  frxpOLD 14604  soseq 14608  axdenselem7 14694  nocvxminlem 14697  axfelem18 14716  axfelem22 14720  symdifass 14731  brsymdif 14732  brsset 14754  dfon3 14757  brbigcup 14759  elfuns 14774  TFSid 14825  FTSid 14826  df3nandALT1 14846  df3nandALT2 14847  andnand1 14848  imnand2 14849  tbw-bijust 14865  rb-bijust 14916  assxor 14979  fampany 14988  boxeq 15022  bidia 15023  albineal 15031  evevifev 15036  repcpwti 15242  deref 15372  efilcp 15688  efilcp2 15692  cnfilca 15693  dmsdtriordOLD 16184  ordisoOLD 16198  ordtypelem7OLD 16205  cptclsscpt 16256  hscptsscld 16258  compfipin0 16260  alexsublem2 16262  alexsublem4 16264  dfcon2 16266  reconn 16275  locfincomp 16338  ist1-3 16367  fbasfip 16380  opnfbas 16381  filfinnfr 16385  filssufillem 16394  ufileu 16397  fixufil 16400  ufinffr 16402  ufilen 16403  filcon 16404  rnelfmlem 16416  fimaxOLD 16570  infmrlb 16589  infmrgelb 16590  wofiOLD 16594  pofunOLD 16596  fdc 16636  nninfnub 16643  heiborlem20 16798  heiborlem38 16816  prtlem80 17071  n0el 17072  2exnaln 17150  2nalexn 17164  2exnexn 17165  2exanali 17167  zfregs2VD 17499  undif3VD 17540  onfrALTlem5VD 17543  cvrval2 17665  cvrnbtwn3 17667  atlrelat1 17718  dalem18 18113  dalem48 18152  cdleme0nex 18661

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 220

Copyright terms: Public domain