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

Theorem notbii 310
Description: Negate both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 19-May-2013.)
Hypothesis
Ref Expression
notbii.1 (𝜑𝜓)
Assertion
Ref Expression
notbii 𝜑 ↔ ¬ 𝜓)

Proof of Theorem notbii
StepHypRef Expression
1 notbii.1 . 2 (𝜑𝜓)
2 notbi 309 . 2 ((𝜑𝜓) ↔ (¬ 𝜑 ↔ ¬ 𝜓))
31, 2mpbi 220 1 𝜑 ↔ ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196
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 197
This theorem is referenced by:  sylnbi  320  xchnxbi  322  xchbinx  324  oplem1  1006  xorcom  1465  xorbi12i  1475  nic-axALT  1597  tbw-bijust  1621  rb-bijust  1672  19.43OLD  1809  cbvexvw  1968  hbn1fw  1970  hba1w  1972  excom  2040  cbvexv1  2174  cbvex  2270  cbvexv  2273  cbvex2  2278  cbvrexf  3161  cbvrexcsf  3559  elsymdifxor  3842  symdifass  3845  dfss4  3850  indifdir  3875  neq0f  3918  ab0  3942  pssdifcom2  4046  difprsnss  4320  brdif  4696  otiunsndisj  4970  difopab  5242  rexiunxp  5251  rexxpf  5258  somin1  5517  cnvdif  5527  difxp  5546  imadif  5961  brprcneu  6171  dffv2  6258  ovima0  6798  porpss  6926  tfinds  7044  poxp  7274  tz7.48lem  7521  brsdom  7963  brsdom2  8069  fimax2g  8191  ordunifi  8195  dfsup2  8335  supgtoreq  8361  infcllem  8378  suc11reg  8501  rankxplim2  8728  rankxplim3  8729  alephval3  8918  kmlem4  8960  cflim2  9070  isfin4-2  9121  fin23lem25  9131  fin1a2lem5  9211  fin12  9220  axcclem  9264  zorng  9311  infinf  9373  alephadd  9384  fpwwe2  9450  axpre-lttri  9971  dfinfre  10989  infrenegsup  10991  arch  11274  rpneg  11848  xmulcom  12081  xmulneg1  12084  xmulf  12087  xrinfmss2  12126  difreicc  12289  fzp1nel  12408  ssnn0fi  12767  fsuppmapnn0fiubex  12775  hashfun  13207  swrdccatin2  13468  s3iunsndisj  13688  incexc2  14551  lcmftp  15330  f1omvdco3  17850  psgnunilem4  17898  0ringnnzr  19250  gsumcom3  20186  mdetunilem7  20405  fctop  20789  cctop  20791  ntreq0  20862  ordtbas2  20976  cmpcld  21186  hausdiag  21429  fbun  21625  fbfinnfr  21626  opnfbas  21627  fbasrn  21669  filuni  21670  ufinffr  21714  alexsubALTlem2  21833  ellogdm  24366  numedglnl  26020  usgredg2v  26100  avril1  27289  shne0i  28277  chnlei  28314  cvnbtwn2  29116  cvnbtwn3  29117  cvnbtwn4  29118  chrelat2i  29194  atabs2i  29231  dmdbr5ati  29251  nmo  29297  difrab2  29311  disjdifprg  29360  eliccelico  29513  elicoelioo  29514  xrdifh  29516  f1ocnt  29533  tosglblem  29643  xrnarchi  29712  hasheuni  30121  cntnevol  30265  sitgaddlemb  30384  eulerpartlemgs2  30416  ballotlem2  30524  ballotlemodife  30533  plymulx0  30598  bnj1143  30835  bnj1304  30864  bnj1476  30891  bnj1533  30896  bnj1174  31045  bnj1204  31054  bnj1280  31062  erdszelem9  31155  dftr6  31615  fundmpss  31640  dfon2lem5  31666  dfon2lem8  31669  dfon2lem9  31670  wzel  31745  wzelOLD  31746  nosepon  31792  noextenddif  31795  nomaxmo  31821  nocvxminlem  31867  elfuns  31997  dfrecs2  32032  gtinfOLD  32289  df3nandALT1  32371  andnand1  32373  imnand2  32374  bj-notalbii  32573  bj-cbvex2v  32713  fdc  33512  nninfnub  33518  tsbi4  33914  ts3an2  33929  ts3an3  33930  ts3or1  33931  n0el  33965  lcvnbtwn2  34133  lcvnbtwn3  34134  cvrnbtwn3  34382  dalem18  34786  lhpocnel2  35124  cdleme0nex  35396  cdlemk19w  36079  dihglblem6  36448  dvh2dim  36553  dvh3dim3N  36557  ctbnfien  37201  rencldnfilem  37203  numinfctb  37492  ifpnorcor  37644  ifpnancor  37645  ifpdfnan  37650  ifpananb  37670  ifpnannanb  37671  ifpxorxorb  37675  rp-fakenanass  37679  rp-isfinite6  37683  pwinfig  37685  elnonrel  37710  iunrelexp0  37813  frege131  38108  frege133  38110  compab  38465  zfregs2VD  38896  undif3VD  38938  onfrALTlem5VD  38941  sineq0ALT  38993  ndisj2  39038  disjrnmpt2  39191  uz0  39452  icccncfext  39863  itgioocnicc  39956  fourierdlem42  40129  fourierdlem62  40148  fourierdlem93  40179  fourierdlem101  40187  nsssmfmbf  40750  otiunsndisjX  41061  nltle2tri  41086  evennodd  41321  setrec2lem1  42205
  Copyright terms: Public domain W3C validator