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

Theorem notbid 307
Description: Deduction negating both sides of a logical equivalence. (Contributed by NM, 21-May-1994.)
Hypothesis
Ref Expression
notbid.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
notbid (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒))

Proof of Theorem notbid
StepHypRef Expression
1 notbid.1 . . 3 (𝜑 → (𝜓𝜒))
2 notnotb 304 . . 3 (𝜓 ↔ ¬ ¬ 𝜓)
3 notnotb 304 . . 3 (𝜒 ↔ ¬ ¬ 𝜒)
41, 2, 33bitr3g 302 . 2 (𝜑 → (¬ ¬ 𝜓 ↔ ¬ ¬ 𝜒))
54con4bid 306 1 (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  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:  notbi  308  annotanannot  959  ifpbi123d  1047  con3ALT  1052  nanbi1  1495  xorbi12d  1518  cbvexvw  2012  hba1wOLD  2017  hbe1w  2018  cbvexv1  2212  cbvex  2308  cbvexv  2311  cbvexd  2314  cbvex2  2316  cbvexdva  2319  drex1  2358  eujustALT  2501  necon3abid  2859  neleq12d  2930  cbvrexf  3196  gencbval  3283  spcegf  3320  spc2gv  3327  spc3gv  3329  cdeqnot  3456  ru  3467  sbcng  3509  sbcrext  3544  sbcrextOLD  3545  cbvrexcsf  3599  difjust  3609  eldif  3617  dfpss3  3726  difeq2  3755  disjne  4055  pssdifcom1  4087  eldifpr  4237  elpwunsn  4256  eldiftp  4260  prel12  4414  prel12g  4418  disjxun  4683  nalset  4828  pwnss  4860  dtru  4887  rexxfrd  4911  rexxfr2d  4913  rexxfrd2  4915  rexxfr  4918  dtruALT  4929  dtruALT2  4941  opthneg  4979  otiunsndisj  5009  poeq1  5067  pocl  5071  swopo  5074  sotric  5090  sotrieq  5091  isso2i  5096  somo  5098  freq1  5113  frirr  5120  fr2nr  5121  frminex  5123  tz7.2  5127  wereu2  5140  poinxp  5216  frinxp  5218  posn  5221  frsn  5223  rexiunxp  5295  rexxpf  5302  intirr  5549  poirr2  5555  cnvpo  5711  predpoirr  5746  predfrirr  5747  nordeq  5780  ordtri1  5794  ordtri3  5797  ordtri3OLD  5798  fvmpti  6320  fndmdif  6361  rexrnmpt  6409  2f1fvneq  6557  f1imapss  6563  cbvexfo  6585  soisoi  6618  isopolem  6635  weniso  6644  canth  6648  riotaclb  6689  rexrnmpt2  6818  ndmovg  6859  sorpssuni  6988  sorpssint  6989  fr3nr  7021  dfwe2  7023  ordsucsssuc  7065  nlimsucg  7084  orduninsuc  7085  dfom2  7109  ssnlim  7125  f1oweALT  7194  frxp  7332  poxp  7334  wfrlem10  7469  smoword  7508  tz7.48lem  7581  oacan  7673  oaword  7674  omlimcl  7703  omeulem1  7707  nnaword  7752  nnmword  7758  nneob  7777  brdifun  7816  swoer  7817  undifixp  7986  boxcutc  7993  2dom  8070  php  8185  nndomo  8195  nnsdomo  8196  unxpdomlem2  8206  frfi  8246  unfilem1  8265  supeq3  8396  supeq123d  8397  supmo  8399  eqsup  8403  supub  8406  sup0  8413  suppr  8418  supisolem  8420  supisoex  8421  eqinf  8431  infval  8433  infmo  8442  infpr  8450  infempty  8453  oieq1  8458  ordtypecbv  8463  ordtypelem7  8470  wemapsolem  8496  canthwdom  8525  zfregcl  8540  elirrv  8542  elirr  8543  noinfep  8595  cantnfp1lem3  8615  rankr1clem  8721  carden2b  8831  domtri2  8853  alephord3  8939  alephdom2  8948  alephval3  8971  dfac9  8996  kmlem2  9011  kmlem4  9013  isfin4  9157  isfin7  9161  fin23lem11  9177  isf32lem5  9217  isf34lem4  9237  fin1a2lem6  9265  fin1a2lem7  9266  fin1a2lem12  9271  itunisuc  9279  ac6n  9345  zorn2g  9363  zornn0g  9365  ttukeylem7  9375  axpowndlem3  9459  axpowndlem4  9460  axregnd  9464  elgch  9482  engch  9488  fpwwe2lem13  9502  fpwwe2  9503  pwfseqlem1  9518  pwfseqlem3  9520  hargch  9533  addnidpi  9761  pinq  9787  nqereu  9789  ltsonq  9829  prlem934  9893  ltexprlem7  9902  addcanpr  9906  prlem936  9907  reclem2pr  9908  reclem3pr  9909  supexpr  9914  ltsosr  9953  supsrlem  9970  axpre-lttri  10024  axpre-sup  10028  xrlenlt  10141  axlttri  10147  axsup  10151  ltne  10172  dedekind  10238  readdcan  10248  leadd1  10534  ltsub1  10562  ltsub2  10563  leord1  10593  lediv1  10926  lemuldiv  10941  lerec  10944  le2msq  10961  infm3  11020  suprnub  11026  infregelb  11045  avgle1  11310  avgle2  11311  znnnlt1  11442  indstr  11794  zsupss  11815  uzsupss  11818  rpneg  11901  xralrple  12074  xleneg  12087  xltadd1  12124  xposdif  12130  xmulneg1  12137  xltmul1  12160  xrsupexmnf  12173  xrinfmexpnf  12174  xrsupsslem  12175  xrinfmsslem  12176  xrub  12180  supxrleub  12194  infxrgelb  12203  difreicc  12342  nn0disj  12494  nelfzo  12514  elfznelfzo  12613  fvinim0ffz  12627  injresinjlem  12628  ssnn0fi  12824  leexp2  12955  hashbnd  13163  hasheni  13176  hashbc  13275  wrdsymb0  13371  swrdnd  13478  swrdnd2  13479  repswswrd  13577  repswccat  13578  cshwidxmod  13595  cnpart  14024  sqrtlt  14046  limsuplt  14254  rlimrege0  14354  isercoll  14442  efle  14892  odd2np1  15112  sumodd  15158  divalglem7  15169  ndvdsadd  15181  fldivndvdslt  15185  bitsfval  15192  bitsval  15193  bits0  15197  bitsp1  15200  bitsmod  15205  bitscmp  15207  bitsinv1lem  15210  sadadd2lem2  15219  saddisjlem  15233  bitsshft  15244  gcdneg  15290  algcvgblem  15337  lcmneg  15363  isprm3  15443  dvdsnprmd  15450  isprm5  15466  rpexp  15479  phiprmpw  15528  m1dvdsndvds  15550  pythagtrip  15586  pcgcd1  15628  prmpwdvds  15655  prmreclem2  15668  prmreclem3  15669  prmreclem5  15671  prmreclem6  15672  vdwlem6  15737  vdwnnlem2  15747  vdwnnlem3  15748  vdwnn  15749  prmo1  15788  prmlem0  15859  prmlem1a  15860  divsfval  16254  mrisval  16337  ismri  16338  ismri2dad  16344  cidpropd  16417  plttr  17017  joinval  17052  meetval  17066  acsfiindd  17224  isnsgrp  17335  mgm2nsgrplem2  17453  sgrp2nmndlem3  17459  symgfix2  17882  pmtrdifellem4  17945  psgnunilem1  17959  psgnunilem5  17960  psgnunilem2  17961  psgnunilem3  17962  pmtrsn  17985  sylow1lem3  18061  sylow2alem2  18079  efgsfo  18198  ablfac1eulem  18517  ablfac1eu  18518  pgpfac1lem1  18519  pgpfac1lem5  18524  islbs  19124  lbsind  19128  lbspss  19130  lbspropd  19147  lspsnne1  19165  islbs2  19202  lbsacsbs  19204  lbsextlem1  19206  lbsextlem3  19208  lbsextlem4  19209  lbsextg  19210  nzrunit  19315  opsrtoslem2  19533  cply1coe0  19717  cply1coe0bi  19718  frlmlbs  20184  islindf  20199  islinds2  20200  islindf2  20201  lindfind  20203  lindsind  20204  lindfrn  20208  lindfmm  20214  lsslindf  20217  islindf4  20225  mdetunilem7  20472  mdetunilem8  20473  mdetunilem9  20474  maducoeval2  20494  pmatcollpw3fi1lem1  20639  fvmptnn04ifa  20703  fvmptnn04ifc  20705  fvmptnn04ifd  20706  chfacffsupp  20709  chfacfscmul0  20711  chfacfpmmul0  20715  elcls  20925  maxlp  20999  perfi  21007  ordtbaslem  21040  ordtval  21041  ordtbas2  21043  ordtopn1  21046  ordtopn2  21047  ordtcnv  21053  ordtrest  21054  ordtrest2lem  21055  ordtrest2  21056  pnfnei  21072  mnfnei  21073  isreg2  21229  ordthauslem  21235  cmpfi  21259  cmpfii  21260  bwth  21261  nconnsubb  21274  hausdiag  21496  txkgen  21503  kqdisj  21583  ordthmeolem  21652  fbfinnfr  21692  trfbas  21695  fbunfip  21720  fbasrn  21735  trfil3  21739  ufileu  21770  fin1aufil  21783  hausflim  21832  alexsubALTlem2  21899  alexsubALTlem3  21900  alexsubALTlem4  21901  ptcmplem2  21904  ptcmplem3  21905  stdbdbl  22369  iccntr  22671  reconnlem2  22677  iccpnfcnv  22790  xrhmeo  22792  lebnumlem1  22807  lebnumlem2  22808  lebnumlem3  22809  bcthlem4  23170  minveclem3b  23245  ivthlem2  23267  ivthlem3  23268  mbfmax  23461  mbfposr  23464  i1fd  23493  mbfi1fseqlem4  23530  itg2splitlem  23560  itg2monolem1  23562  itg2cnlem1  23573  dvne0  23819  lhop1lem  23821  deg1nn0clb  23895  dgrle  24044  coemulhi  24055  aaliou3lem9  24150  cos11  24324  logleb  24394  argrege0  24402  logdivle  24413  ellogdm  24430  cxple  24486  cxplt2  24489  cxple3  24492  isosctrlem1  24593  atandm  24648  atans2  24703  atantayl2  24710  eldmgm  24793  ftalem7  24850  isppw2  24886  musum  24962  dchrsum2  25038  bposlem1  25054  lgsmod  25093  lgsdir2lem2  25096  lgsdir2  25100  lgsne0  25105  lgsprme0  25109  gausslemma2dlem4  25139  lgsquadlem1  25150  2lgslem3  25174  2lgsoddprm  25186  rpvmasumlem  25221  padicabv  25364  ostth3  25372  ostth  25373  istrkgld  25403  axtgupdim2  25415  tglowdim2l  25590  axlowdimlem16  25882  axlowdim2  25885  axlowdim  25886  numedglnl  26084  usgredg2v  26164  lfuhgr1v0e  26191  cusgrfi  26410  vtxd0nedgb  26440  vtxduhgr0edgnel  26446  1loopgrnb0  26454  1hevtxdg0  26457  vtxdgoddnumeven  26505  wlkp1lem1  26626  wlkp1lem2  26627  wlkp1lem5  26630  crctcsh  26772  clwwlknclwwlkdifsOLD  26947  clwlkclwwlklem2a4  26963  eupth2eucrct  27195  eupth2lem3lem3  27208  eupth2lem3lem4  27209  eupth2lem3lem6  27211  eupth2lem3lem7  27212  eupth2lems  27216  eupth2  27217  konigsberglem4  27233  nfrgr2v  27252  frgrwopreglem3  27294  fusgr2wsp2nb  27314  frgrreggt1  27380  friendshipgt3  27385  lpni  27462  nmobndseqi  27762  minvecolem5  27865  chpsscon3  28490  chnle  28501  nonbooli  28638  pjnel  28713  specval  28885  nmcfnlbi  29039  stri  29244  hstri  29252  cvbr  29269  cvcon3  29271  chcv1  29342  cvexchlem  29355  chrelat2  29357  spc2d  29441  elpreq  29486  ifeqeqx  29487  isoun  29607  suppss3  29630  xrge0infss  29653  infxrge0gelb  29659  eliccelico  29667  elicoelioo  29668  nndiffz1  29676  nn0min  29695  toslublem  29795  tosglblem  29797  isarchi2  29867  archiabl  29880  ordtcnvNEW  30094  ordtrestNEW  30095  ordtrest2NEWlem  30096  ordtrest2NEW  30097  ordtconnlem1  30098  xrge0iifcnv  30107  elzdif0  30152  esumpcvgval  30268  esum2d  30283  ddemeas  30427  omssubadd  30490  oddpwdc  30544  eulerpartlems  30550  eulerpartlemf  30560  eulerpartlemt  30561  eulerpartlemr  30564  eulerpartlemgvv  30566  eulerpartlemn  30571  ballotlemfc0  30682  ballotlemfcc  30683  ballotlem4  30688  ballotlemimin  30695  ballotlem7  30725  plymulx  30753  signsply0  30756  reprinfz1  30828  reprpmtf1o  30832  reprdifc  30833  hgt750lema  30863  hgt750leme  30864  istrkg2d  30872  bnj23  30912  bnj1185  30990  bnj1228  31205  bnj1388  31227  bnj1417  31235  erdszelem10  31308  ismfs  31572  mvtinf  31578  untelirr  31711  untsucf  31713  untangtr  31717  ceqsralv2  31733  inffzOLD  31741  dfpo2  31771  dfon2lem3  31814  dfon2lem4  31815  dfon2lem7  31818  dfon2lem9  31820  distel  31833  frpomin  31863  soseq  31879  noextenddif  31946  nodenselem4  31962  nodenselem5  31963  nodenselem7  31965  nolt02o  31970  noresle  31971  noprefixmo  31973  nosupdm  31975  nosupfv  31977  nosupres  31978  nosupbnd1lem1  31979  nosupbnd1lem3  31981  nosupbnd1lem5  31983  nosupbnd1  31985  nosupbnd2lem1  31986  nosupbnd2  31987  slenlt  32002  nocvxminlem  32018  slerec  32048  funpartfv  32177  dfrdg4  32183  nn0prpwlem  32442  nn0prpw  32443  limsucncmpi  32569  limsucncmp  32570  ordcmp  32571  unblimceq0  32623  unbdqndv1  32624  bj-hbntbi  32820  bj-cbvexdv  32861  bj-cbvex2v  32863  bj-drex1v  32874  bj-nalset  32919  bj-dtru  32922  bj-ru0  33057  bj-nuliota  33144  topdifinffinlem  33325  topdifinffin  33326  icorempt2  33329  relowlpssretop  33342  finxpreclem2  33357  finxpreclem6  33363  wl-ax11-lem8  33499  leceifl  33528  lindsenlbs  33534  matunitlindflem1  33535  poimirlem16  33555  poimirlem17  33556  poimirlem18  33557  poimirlem19  33558  poimirlem21  33560  poimirlem23  33562  poimirlem26  33565  poimirlem27  33566  poimirlem28  33567  poimirlem31  33570  poimir  33572  mblfinlem2  33577  mblfinlem3  33578  ismblfin  33580  cnambfre  33588  itg2addnclem  33591  itg2addnclem2  33592  iblabsnclem  33603  ftc1anclem1  33615  areacirc  33635  heibor1lem  33738  heiborlem1  33740  heiborlem6  33745  heiborlem8  33747  heiborlem10  33749  smprngopr  33981  ecin0  34257  ax12inda  34552  riotaclbgBAD  34558  lcvfbr  34625  lcvbr  34626  lsatcv0  34636  l1cvpat  34659  opltcon3b  34809  cvrfval  34873  cvrval  34874  cvrnbtwn  34876  cvrval2  34879  cvrnbtwn2  34880  cvrnbtwn3  34881  cvrcon3b  34882  cvrnbtwn4  34884  atnlt  34918  iscvlat  34928  cvlexch1  34933  hlsuprexch  34985  hlrelat5N  35005  hlrelat2  35007  cvrval5  35019  3dimlem1  35062  3dim1lem5  35070  3dim2  35072  3dim3  35073  llnnlt  35127  islpln5  35139  lplni2  35141  lvolex3N  35142  lplnnle2at  35145  islpln2a  35152  lplnribN  35155  lplnexllnN  35168  lplnnlt  35169  lvoli3  35181  islvol5  35183  lvoli2  35185  lvolnle3at  35186  islvol2aN  35196  4atlem11  35213  lvolnltN  35222  dalawlem15  35489  4atexlemex2  35675  4atex  35680  4atex2-0aOLDN  35682  4atex2-0cOLDN  35684  lautcvr  35696  ltrnfset  35721  ltrnset  35722  ltrnu  35725  trlfset  35765  trlset  35766  trlval2  35768  cdlemd6  35808  cdleme0nex  35895  cdleme18d  35900  cdleme25b  35959  cdleme25cv  35963  cdleme29b  35980  cdleme31fv  35995  cdleme31fv2  35998  cdlemefrs29bpre0  36001  cdlemefr32sn2aw  36009  cdlemefr29bpre0N  36011  cdlemefr29clN  36012  cdlemefr32fvaN  36014  cdlemefr32fva1  36015  cdlemefs32sn1aw  36019  cdleme32fva  36042  cdleme32fvaw  36044  cdleme40v  36074  cdleme42b  36083  cdleme46f2g2  36098  cdleme46f2g1  36099  cdleme48gfv  36142  cdlemg1fvawlemN  36178  cdlemg1cex  36193  cdlemg6d  36226  cdlemm10N  36724  dicffval  36780  dicfval  36781  dicval  36782  dicfnN  36789  dicvalrelN  36791  dihffval  36836  dihfval  36837  dihlsscpre  36840  dvh4dimat  37044  dvh3dimatN  37045  dvh4dimlem  37049  dvh3dim  37052  dvh4dimN  37053  dvh3dim2  37054  dvh3dim3N  37055  mapdcv  37266  mapdh9aOLDN  37397  hdmapfval  37436  hdmapval  37437  hdmapval2  37441  hdmap11lem2  37451  ellz1  37647  rencldnfilem  37701  jm2.22  37879  jm2.23  37880  wepwsolem  37929  fnwe2lem2  37938  aomclem8  37948  unxpwdom3  37982  ifpbi12  38150  ifpbi123  38152  relintabex  38204  ss2iundf  38268  frege124d  38370  clsk3nimkb  38655  clsk1indlem1  38660  clsk1independent  38661  ntrneineine1lem  38699  ntrneicls11  38705  clsneiel1  38723  clsneiel2  38724  neicvgel1  38734  neicvgel2  38735  radcnvrat  38830  rusbcALT  38957  en3lpVD  39394  eliin2f  39601  nssd  39602  wessf1ornlem  39685  limsupre2lem  40274  icccncfext  40418  stoweidlem14  40549  stoweidlem34  40569  stoweidlem59  40594  etransclem24  40793  nnfoctbdjlem  40990  nnfoctbdj  40991  hspmbllem2  41162  smfmbfcex  41289  nsssmfmbflem  41307  eu2ndop1stv  41523  afvfv0bi  41553  afvco2  41577  ndmaovg  41585  nelbr  41615  otiunsndisjX  41621  fun2dmnopgexmpl  41626  ltnltne  41638  fmtnoinf  41773  odz2prm2pw  41800  prmdvdsfmtnof1lem2  41822  lighneallem3  41849  lighneallem4  41852  isodd3  41890  bits0ALTV  41915  lidldomnnring  42255  zrninitoringc  42396  ztprmneprm  42450  lindepsnlininds  42566  islindeps  42567  lindslinindsimp2lem5  42576  lindslinindsimp2  42577  difmodm1lt  42642  elsetrecslem  42770
  Copyright terms: Public domain W3C validator