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

Theorem notbid 319
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 316 . . 3 (𝜓 ↔ ¬ ¬ 𝜓)
3 notnotb 316 . . 3 (𝜒 ↔ ¬ ¬ 𝜒)
41, 2, 33bitr3g 314 . 2 (𝜑 → (¬ ¬ 𝜓 ↔ ¬ ¬ 𝜒))
54con4bid 318 1 (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207
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 208
This theorem is referenced by:  notbi  320  annotanannot  830  ifpbi123d  1069  con3ALT  1076  con3ALTOLD  1077  xorbi12d  1509  norassOLD  1525  equsexvw  2002  cbvexvw  2035  cbvexdvaw  2037  hbe1w  2046  cbvexv1  2353  cbvex2v  2356  drex1v  2379  cbvex  2408  cbvexvOLD  2412  cbvex2  2425  drex1  2455  eujustALT  2650  necon3abid  3049  neleq12d  3124  cbvrexfw  3436  cbvrexf  3438  cbvrexdva2OLD  3456  gencbval  3549  spcegf  3588  spc2gv  3598  spc2d  3600  spc3gv  3602  cdeqnot  3756  rru  3767  ru  3768  sbcng  3816  sbcrext  3853  cbvrexcsf  3923  difjust  3935  eldif  3943  dfpss3  4060  dfdif3  4088  difeq2  4090  disjne  4400  pssdifcom1  4431  eldifpr  4587  elpwunsn  4613  eldiftp  4616  preqsnd  4781  disjxun  5055  nalset  5208  dtru  5262  dtruALT  5279  rexxfrd  5300  rexxfr2d  5302  rexxfrd2  5304  rexxfr  5307  dtruALT2  5326  opthneg  5364  snopeqop  5387  otiunsndisj  5401  poeq1  5470  pocl  5474  swopo  5477  sotric  5494  sotrieq  5495  isso2i  5501  somo  5503  freq1  5518  frirr  5525  fr2nr  5526  frminex  5528  tz7.2  5532  wereu2  5545  poinxp  5625  frinxp  5627  posn  5630  frsn  5632  rexiunxp  5704  rexxpf  5711  intirr  5971  poirr2  5977  cnvpo  6131  predpoirr  6169  predfrirr  6170  nordeq  6203  ordtri1  6217  ordtri3  6220  fvmpti  6760  fndmdif  6804  rexrnmptw  6853  rexrnmpt  6855  2f1fvneq  7009  f1imapss  7015  cbvexfo  7037  soisoi  7070  isopolem  7087  weniso  7096  canth  7100  riotaclb  7144  rexrnmpo  7279  ndmovg  7320  sorpssuni  7447  sorpssint  7448  fr3nr  7483  dfwe2  7485  ordsucsssuc  7527  nlimsucg  7546  orduninsuc  7547  dfom2  7571  ssnlim  7588  f1oweALT  7662  frxp  7809  poxp  7811  suppofssd  7856  wfrlem10  7953  smoword  7992  tz7.48lem  8066  oacan  8163  oaword  8164  omlimcl  8193  omeulem1  8197  nnaword  8242  nnmword  8248  nneob  8268  brdifun  8307  swoer  8308  undifixp  8486  boxcutc  8493  2dom  8570  php  8689  nndomo  8700  nnsdomo  8701  unxpdomlem2  8711  frfi  8751  unfilem1  8770  supeq3  8901  supeq123d  8902  supmo  8904  eqsup  8908  supub  8911  sup0  8918  suppr  8923  supisolem  8925  supisoex  8926  eqinf  8936  infval  8938  infmo  8947  infpr  8955  infempty  8959  oieq1  8964  ordtypecbv  8969  ordtypelem7  8976  wemapsolem  9002  canthwdom  9031  zfregcl  9046  elirrv  9048  elirr  9049  noinfep  9111  cantnfp1lem3  9131  rankr1clem  9237  carden2b  9384  domtri2  9406  alephord3  9492  alephdom2  9501  alephval3  9524  dfac9  9550  kmlem2  9565  kmlem4  9567  isfin4  9707  isfin7  9711  fin23lem11  9727  isf32lem5  9767  isf34lem4  9787  fin1a2lem6  9815  fin1a2lem7  9816  fin1a2lem12  9821  itunisuc  9829  ac6n  9895  zorn2g  9913  zornn0g  9915  ttukeylem7  9925  axpowndlem3  10009  axpowndlem4  10010  axregnd  10014  elgch  10032  engch  10038  fpwwe2lem13  10052  fpwwe2  10053  pwfseqlem1  10068  pwfseqlem3  10070  hargch  10083  addnidpi  10311  pinq  10337  nqereu  10339  ltsonq  10379  prlem934  10443  ltexprlem7  10452  addcanpr  10456  prlem936  10457  reclem2pr  10458  reclem3pr  10459  supexpr  10464  ltsosr  10504  supsrlem  10521  axpre-lttri  10575  axpre-sup  10579  xrlenlt  10694  axlttri  10700  axsup  10704  ltne  10725  dedekind  10791  readdcan  10802  leadd1  11096  ltsub1  11124  ltsub2  11125  leord1  11155  lediv1  11493  lemuldiv  11508  lerec  11511  le2msq  11528  infm3  11588  suprnub  11594  infregelb  11613  avgle1  11865  avgle2  11866  znnnlt1  11997  indstr  12304  zsupss  12325  uzsupss  12328  rpneg  12409  xralrple  12586  xleneg  12599  xltadd1  12637  xposdif  12643  xmulneg1  12650  xltmul1  12673  xrsupexmnf  12686  xrinfmexpnf  12687  xrsupsslem  12688  xrinfmsslem  12689  xrub  12693  supxrleub  12707  infxrgelb  12716  difreicc  12858  nn0disj  13011  nelfzo  13031  elfznelfzo  13130  fvinim0ffz  13144  injresinjlem  13145  ssnn0fi  13341  leexp2  13523  hashbnd  13684  hasheni  13696  hashbc  13799  wrdsymb0  13889  swrdnd  14004  swrdnd2  14005  pfxnd0  14038  repswswrd  14134  repswccat  14136  cshwidxmod  14153  cnpart  14587  sqrtlt  14609  limsuplt  14824  rlimrege0  14924  isercoll  15012  efle  15459  odd2np1  15678  sumodd  15727  divalglem7  15738  ndvdsadd  15749  fldivndvdslt  15753  bitsfval  15760  bitsval  15761  bits0  15765  bitsp1  15768  bitsmod  15773  bitscmp  15775  bitsinv1lem  15778  sadadd2lem2  15787  saddisjlem  15801  bitsshft  15812  gcdneg  15858  algcvgblem  15909  lcmneg  15935  isprm3  16015  dvdsnprmd  16022  isprm5  16039  rpexp  16052  phiprmpw  16101  m1dvdsndvds  16123  pythagtrip  16159  pcgcd1  16201  prmpwdvds  16228  prmreclem2  16241  prmreclem3  16242  prmreclem5  16244  prmreclem6  16245  vdwlem6  16310  vdwnnlem2  16320  vdwnnlem3  16321  vdwnn  16322  prmlem0  16427  prmlem1a  16428  divsfval  16808  mrisval  16889  ismri  16890  ismri2dad  16896  cidpropd  16968  plttr  17568  joinval  17603  meetval  17617  acsfiindd  17775  isnsgrp  17893  mgm2nsgrplem2  18022  sgrp2nmndlem3  18028  symgfix2  18473  pmtrdifellem4  18536  psgnunilem1  18550  psgnunilem5  18551  psgnunilem2  18552  psgnunilem3  18553  pmtrsn  18576  sylow1lem3  18654  sylow2alem2  18672  efgsfo  18794  ablfac1eulem  19123  ablfac1eu  19124  pgpfac1lem1  19125  pgpfac1lem5  19130  islbs  19777  lbsind  19781  lbspss  19783  lbspropd  19800  lspsnne1  19818  islbs2  19855  lbsacsbs  19857  lbsextlem1  19859  lbsextlem3  19861  lbsextlem4  19862  lbsextg  19863  nzrunit  19968  opsrtoslem2  20193  cply1coe0  20395  cply1coe0bi  20396  frlmlbs  20869  islindf  20884  islinds2  20885  islindf2  20886  lindfind  20888  lindsind  20889  lindfrn  20893  lindfmm  20899  lsslindf  20902  islindf4  20910  mdetunilem7  21155  mdetunilem8  21156  mdetunilem9  21157  maducoeval2  21177  pmatcollpw3fi1lem1  21322  fvmptnn04ifa  21386  fvmptnn04ifc  21388  fvmptnn04ifd  21389  chfacffsupp  21392  chfacfscmul0  21394  chfacfpmmul0  21398  elcls  21609  maxlp  21683  perfi  21691  ordtbaslem  21724  ordtval  21725  ordtbas2  21727  ordtopn1  21730  ordtopn2  21731  ordtcnv  21737  ordtrest  21738  ordtrest2lem  21739  ordtrest2  21740  pnfnei  21756  mnfnei  21757  isreg2  21913  ordthauslem  21919  cmpfi  21944  cmpfii  21945  bwth  21946  nconnsubb  21959  hausdiag  22181  txkgen  22188  kqdisj  22268  ordthmeolem  22337  fbfinnfr  22377  trfbas  22380  fbunfip  22405  fbasrn  22420  trfil3  22424  ufileu  22455  fin1aufil  22468  hausflim  22517  alexsubALTlem2  22584  alexsubALTlem3  22585  alexsubALTlem4  22586  ptcmplem2  22589  ptcmplem3  22590  stdbdbl  23054  iccntr  23356  reconnlem2  23362  iccpnfcnv  23475  xrhmeo  23477  lebnumlem1  23492  lebnumlem2  23493  lebnumlem3  23494  bcthlem4  23857  minveclem3b  23958  ivthlem2  23980  ivthlem3  23981  mbfmax  24177  mbfposr  24180  i1fd  24209  mbfi1fseqlem4  24246  itg2splitlem  24276  itg2monolem1  24278  itg2cnlem1  24289  dvne0  24535  lhop1lem  24537  deg1nn0clb  24611  dgrle  24760  coemulhi  24771  aaliou3lem9  24866  cos11  25044  logleb  25113  argrege0  25121  logdivle  25132  ellogdm  25149  cxple  25205  cxplt2  25208  cxple3  25211  isosctrlem1  25323  atandm  25381  atans2  25436  atantayl2  25443  eldmgm  25526  ftalem7  25583  isppw2  25619  musum  25695  dchrsum2  25771  bposlem1  25787  lgsmod  25826  lgsdir2lem2  25829  lgsdir2  25833  lgsne0  25838  lgsprme0  25842  gausslemma2dlem4  25872  lgsquadlem1  25883  2lgslem3  25907  2lgsoddprm  25919  2sq2  25936  addsqrexnreu  25945  rpvmasumlem  25990  padicabv  26133  ostth3  26141  ostth  26142  istrkgld  26172  axtgupdim2  26184  tglowdim2l  26363  axlowdimlem16  26670  axlowdim2  26673  axlowdim  26674  numedglnl  26856  usgredg2v  26936  lfuhgr1v0e  26963  cusgrfi  27167  vtxd0nedgb  27197  vtxduhgr0edgnel  27203  1loopgrnb0  27211  1hevtxdg0  27214  vtxdgoddnumeven  27262  wlkp1lem1  27382  wlkp1lem2  27383  wlkp1lem5  27386  crctcsh  27529  clwlkclwwlklem2a4  27702  eupth2eucrct  27923  eupth2lem3lem3  27936  eupth2lem3lem4  27937  eupth2lem3lem6  27939  eupth2lem3lem7  27940  eupth2lems  27944  eupth2  27945  konigsberglem4  27961  nfrgr2v  27978  frgrwopreglem3  28020  fusgr2wsp2nb  28040  frgrreggt1  28099  friendshipgt3  28104  lpni  28184  nmobndseqi  28483  minvecolem5  28585  chpsscon3  29207  chnle  29218  nonbooli  29355  pjnel  29430  specval  29602  nmcfnlbi  29756  stri  29961  hstri  29969  cvbr  29986  cvcon3  29988  chcv1  30059  cvexchlem  30072  chrelat2  30074  nelun  30201  elpreq  30217  nelpr  30218  ifeqeqx  30224  nfpconfp  30305  isoun  30363  suppss3  30386  xrge0infss  30410  infxrge0gelb  30416  eliccelico  30426  elicoelioo  30427  nndiffz1  30435  hashgt1  30456  nn0min  30463  toslublem  30581  tosglblem  30583  pmtrcnel  30660  cycpmco2  30702  isarchi2  30741  archiabl  30754  0nellinds  30862  lindssn  30866  lindfpropd  30869  lbslsat  30913  lindsunlem  30919  ordtcnvNEW  31062  ordtrestNEW  31063  ordtrest2NEWlem  31064  ordtrest2NEW  31065  ordtconnlem1  31066  xrge0iifcnv  31075  esumpcvgval  31236  esum2d  31251  ddemeas  31394  omssubadd  31457  oddpwdc  31511  eulerpartlems  31517  eulerpartlemf  31527  eulerpartlemt  31528  eulerpartlemr  31531  eulerpartlemgvv  31533  eulerpartlemn  31538  ballotlemfc0  31649  ballotlemfcc  31650  ballotlem4  31655  ballotlemimin  31662  ballotlem7  31692  plymulx  31717  signsply0  31720  reprinfz1  31792  reprpmtf1o  31796  reprdifc  31797  hgt750lema  31827  hgt750leme  31828  istrkg2d  31836  bnj23  31887  bnj1185  31964  bnj1228  32180  bnj1388  32202  bnj1417  32210  hashfundm  32251  revwlk  32268  isacycgr  32289  acycgr0v  32292  prclisacycgr  32295  erdszelem10  32344  satf0n0  32522  fmlaomn0  32534  fmlasucdisj  32543  satfv1fvfmla1  32567  satefvfmla1  32569  ismfs  32693  mvtinf  32699  untelirr  32831  untsucf  32833  untangtr  32837  ceqsralv2  32853  dfpo2  32888  dfon2lem3  32927  dfon2lem4  32928  dfon2lem7  32931  dfon2lem9  32933  distel  32945  frpomin  32975  soseq  32993  noextenddif  33072  nodenselem4  33088  nodenselem5  33089  nodenselem7  33091  nolt02o  33096  noresle  33097  noprefixmo  33099  nosupdm  33101  nosupfv  33103  nosupres  33104  nosupbnd1lem1  33105  nosupbnd1lem3  33107  nosupbnd1lem5  33109  nosupbnd1  33111  nosupbnd2lem1  33112  nosupbnd2  33113  slenlt  33128  nocvxminlem  33144  slerec  33174  funpartfv  33303  dfrdg4  33309  nn0prpwlem  33567  nn0prpw  33568  limsucncmpi  33690  limsucncmp  33691  ordcmp  33692  unblimceq0  33743  unbdqndv1  33744  bj-hbntbi  33935  bj-cbvexdv  34019  bj-dtru  34036  bj-ru0  34150  bj-nuliota  34244  topdifinffinlem  34510  topdifinffin  34511  icorempo  34514  relowlpssretop  34527  finxpreclem2  34553  finxpreclem6  34559  wl-ax11-lem8  34705  wl-dfrexf  34728  leceifl  34762  lindsadd  34766  lindsenlbs  34768  matunitlindflem1  34769  poimirlem16  34789  poimirlem17  34790  poimirlem18  34791  poimirlem19  34792  poimirlem21  34794  poimirlem23  34796  poimirlem26  34799  poimirlem27  34800  poimirlem28  34801  poimirlem31  34804  poimir  34806  mblfinlem2  34811  mblfinlem3  34812  ismblfin  34814  cnambfre  34821  itg2addnclem  34824  itg2addnclem2  34825  iblabsnclem  34836  ftc1anclem1  34848  areacirc  34868  heibor1lem  34968  heiborlem1  34970  heiborlem6  34975  heiborlem8  34977  heiborlem10  34979  smprngopr  35211  ecin0  35487  ax12inda  35964  riotaclbgBAD  35970  lcvfbr  36036  lcvbr  36037  lsatcv0  36047  l1cvpat  36070  opltcon3b  36220  cvrfval  36284  cvrval  36285  cvrnbtwn  36287  cvrval2  36290  cvrnbtwn2  36291  cvrnbtwn3  36292  cvrcon3b  36293  cvrnbtwn4  36295  atnlt  36329  iscvlat  36339  cvlexch1  36344  hlsuprexch  36397  hlrelat5N  36417  hlrelat2  36419  cvrval5  36431  3dimlem1  36474  3dim1lem5  36482  3dim2  36484  3dim3  36485  llnnlt  36539  islpln5  36551  lplni2  36553  lvolex3N  36554  lplnnle2at  36557  islpln2a  36564  lplnribN  36567  lplnexllnN  36580  lplnnlt  36581  lvoli3  36593  islvol5  36595  lvoli2  36597  lvolnle3at  36598  islvol2aN  36608  4atlem11  36625  lvolnltN  36634  dalawlem15  36901  4atexlemex2  37087  4atex  37092  4atex2-0aOLDN  37094  4atex2-0cOLDN  37096  lautcvr  37108  ltrnfset  37133  ltrnset  37134  ltrnu  37137  trlfset  37176  trlset  37177  trlval2  37179  cdlemd6  37219  cdleme0nex  37306  cdleme18d  37311  cdleme25b  37370  cdleme25cv  37374  cdleme29b  37391  cdleme31fv  37406  cdleme31fv2  37409  cdlemefrs29bpre0  37412  cdlemefr32sn2aw  37420  cdlemefr29bpre0N  37422  cdlemefr29clN  37423  cdlemefr32fvaN  37425  cdlemefr32fva1  37426  cdlemefs32sn1aw  37430  cdleme32fva  37453  cdleme32fvaw  37455  cdleme40v  37485  cdleme42b  37494  cdleme46f2g2  37509  cdleme46f2g1  37510  cdleme48gfv  37553  cdlemg1fvawlemN  37589  cdlemg1cex  37604  cdlemg6d  37637  cdlemm10N  38134  dicffval  38190  dicfval  38191  dicval  38192  dicfnN  38199  dicvalrelN  38201  dihffval  38246  dihfval  38247  dihlsscpre  38250  dvh4dimat  38454  dvh3dimatN  38455  dvh4dimlem  38459  dvh3dim  38462  dvh4dimN  38463  dvh3dim2  38464  dvh3dim3N  38465  mapdcv  38676  mapdh9aOLDN  38806  hdmapfval  38843  hdmapval  38844  hdmapval2  38848  hdmap11lem2  38858  oexpreposd  39057  ellz1  39242  rencldnfilem  39295  jm2.22  39470  jm2.23  39471  wepwsolem  39520  fnwe2lem2  39529  aomclem8  39539  unxpwdom3  39573  ifpbi12  39732  dfsucon  39767  nndomog  39775  ss2iundf  39882  frege124d  39984  clsk3nimkb  40268  clsk1indlem1  40273  clsk1independent  40274  ntrneineine1lem  40312  ntrneicls11  40318  clsneiel1  40336  clsneiel2  40337  neicvgel1  40347  neicvgel2  40348  radcnvrat  40523  rusbcALT  40648  en3lpVD  41056  eliin2f  41247  nssd  41248  wessf1ornlem  41321  limsupre2lem  41881  icccncfext  42046  stoweidlem14  42176  stoweidlem34  42196  stoweidlem59  42221  etransclem24  42420  nnfoctbdjlem  42614  nnfoctbdj  42615  hspmbllem2  42786  smfmbfcex  42913  nsssmfmbflem  42931  eu2ndop1stv  43201  afvfv0bi  43228  afvco2  43252  ndmaovg  43260  ndfatafv2nrn  43297  afv2ndefb  43300  afv2fv0  43341  nelbr  43350  otiunsndisjX  43355  fun2dmnopgexmpl  43360  ltnltne  43376  readdcnnred  43380  resubcnnred  43381  recnmulnred  43382  cndivrenred  43383  ichnreuop  43511  fmtnoinf  43575  odz2prm2pw  43602  prmdvdsfmtnof1lem2  43624  lighneallem3  43649  lighneallem4  43652  requad1  43664  isodd3  43694  bits0ALTV  43721  nfermltl8rev  43784  nfermltl2rev  43785  nfermltlrev  43786  smndex1n0mnd  44012  lidldomnnring  44129  zrninitoringc  44270  ztprmneprm  44323  lindepsnlininds  44435  islindeps  44436  lindslinindsimp2lem5  44445  lindslinindsimp2  44446  difmodm1lt  44510  line2ylem  44666  line2xlem  44668  elsetrecslem  44729
  Copyright terms: Public domain W3C validator