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

Theorem notbid 308
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 307 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  309  ifpbi123d  1027  con3ALT  1032  con3OLD  1035  nanbi1  1454  xorbi12d  1477  cbvexvw  1969  hba1wOLD  1974  hbe1w  1975  cbvexv1  2175  cbvex  2271  cbvexv  2274  cbvexd  2277  cbvex2  2279  cbvexdva  2282  drex1  2326  eujustALT  2472  necon3abid  2829  neleq12d  2900  cbvrexf  3164  gencbval  3250  spcegf  3287  spc2gv  3294  spc3gv  3296  cdeqnot  3421  ru  3432  sbcng  3474  sbcrext  3509  sbcrextOLD  3510  cbvrexcsf  3564  difjust  3574  eldif  3582  dfpss3  3691  difeq2  3720  disjne  4020  pssdifcom1  4052  eldifpr  4202  elpwunsn  4222  eldiftp  4226  prel12  4381  prel12g  4385  disjxun  4649  nalset  4793  pwnss  4828  dtru  4855  rexxfrd  4879  rexxfr2d  4881  rexxfrd2  4883  rexxfr  4886  dtruALT  4897  dtruALT2  4909  opthneg  4948  otiunsndisj  4978  poeq1  5036  pocl  5040  swopo  5043  sotric  5059  sotrieq  5060  isso2i  5065  somo  5067  freq1  5082  frirr  5089  fr2nr  5090  frminex  5092  tz7.2  5096  wereu2  5109  poinxp  5180  frinxp  5182  posn  5185  frsn  5187  rexiunxp  5260  rexxpf  5267  intirr  5512  poirr2  5518  cnvpo  5671  predpoirr  5706  predfrirr  5707  nordeq  5740  ordtri1  5754  ordtri3  5757  ordtri3OLD  5758  fvmpti  6279  fndmdif  6319  rexrnmpt  6367  2f1fvneq  6514  f1imapss  6520  cbvexfo  6542  soisoi  6575  isopolem  6592  weniso  6601  canth  6605  riotaclb  6646  rexrnmpt2  6773  ndmovg  6814  sorpssuni  6943  sorpssint  6944  fr3nr  6976  dfwe2  6978  ordsucsssuc  7020  nlimsucg  7039  orduninsuc  7040  dfom2  7064  ssnlim  7080  f1oweALT  7149  frxp  7284  poxp  7286  wfrlem10  7421  smoword  7460  tz7.48lem  7533  oacan  7625  oaword  7626  omlimcl  7655  omeulem1  7659  nnaword  7704  nnmword  7710  nneob  7729  brdifun  7768  swoer  7769  undifixp  7941  boxcutc  7948  2dom  8026  php  8141  nndomo  8151  nnsdomo  8152  unxpdomlem2  8162  frfi  8202  unfilem1  8221  supeq3  8352  supeq123d  8353  supmo  8355  eqsup  8359  supub  8362  sup0  8369  suppr  8374  supisolem  8376  supisoex  8377  eqinf  8387  infval  8389  infmo  8398  infpr  8406  infempty  8409  oieq1  8414  ordtypecbv  8419  ordtypelem7  8426  wemapsolem  8452  canthwdom  8481  zfregcl  8496  zfregclOLD  8498  elirrv  8501  elirr  8502  noinfep  8554  cantnfp1lem3  8574  rankr1clem  8680  carden2b  8790  domtri2  8812  alephord3  8898  alephdom2  8907  alephval3  8930  dfac9  8955  kmlem2  8970  kmlem4  8972  isfin4  9116  isfin7  9120  fin23lem11  9136  isf32lem5  9176  isf34lem4  9196  fin1a2lem6  9224  fin1a2lem7  9225  fin1a2lem12  9230  itunisuc  9238  ac6n  9304  zorn2g  9322  zornn0g  9324  ttukeylem7  9334  axpowndlem3  9418  axpowndlem4  9419  axregnd  9423  elgch  9441  engch  9447  fpwwe2lem13  9461  fpwwe2  9462  pwfseqlem1  9477  pwfseqlem3  9479  hargch  9492  addnidpi  9720  pinq  9746  nqereu  9748  ltsonq  9788  prlem934  9852  ltexprlem7  9861  addcanpr  9865  prlem936  9866  reclem2pr  9867  reclem3pr  9868  supexpr  9873  ltsosr  9912  supsrlem  9929  axpre-lttri  9983  axpre-sup  9987  xrlenlt  10100  axlttri  10106  axsup  10110  ltne  10131  dedekind  10197  readdcan  10207  leadd1  10493  ltsub1  10521  ltsub2  10522  leord1  10552  lediv1  10885  lemuldiv  10900  lerec  10903  le2msq  10920  infm3  10979  suprnub  10985  infregelb  11004  avgle1  11269  avgle2  11270  znnnlt1  11401  indstr  11753  zsupss  11774  uzsupss  11777  rpneg  11860  xralrple  12033  xleneg  12046  xltadd1  12083  xposdif  12089  xmulneg1  12096  xltmul1  12119  xrsupexmnf  12132  xrinfmexpnf  12133  xrsupsslem  12134  xrinfmsslem  12135  xrub  12139  supxrleub  12153  infxrgelb  12162  difreicc  12301  nn0disj  12451  nelfzo  12471  elfznelfzo  12569  fvinim0ffz  12582  injresinjlem  12583  ssnn0fi  12779  leexp2  12910  hashbnd  13118  hasheni  13131  hashbc  13232  wrdsymb0  13334  swrdnd  13426  swrdnd2  13427  repswswrd  13525  repswccat  13526  cshwidxmod  13543  cnpart  13974  sqrtlt  13996  limsuplt  14204  rlimrege0  14304  isercoll  14392  efle  14842  odd2np1  15059  sumodd  15105  divalglem7  15116  ndvdsadd  15128  fldivndvdslt  15132  bitsfval  15139  bitsval  15140  bits0  15144  bitsp1  15147  bitsmod  15152  bitscmp  15154  bitsinv1lem  15157  sadadd2lem2  15166  saddisjlem  15180  bitsshft  15191  gcdneg  15237  algcvgblem  15284  lcmneg  15310  isprm3  15390  dvdsnprmd  15397  isprm5  15413  rpexp  15426  phiprmpw  15475  m1dvdsndvds  15497  pythagtrip  15533  pcgcd1  15575  prmpwdvds  15602  prmreclem2  15615  prmreclem3  15616  prmreclem5  15618  prmreclem6  15619  vdwlem6  15684  vdwnnlem2  15694  vdwnnlem3  15695  vdwnn  15696  prmo1  15735  prmlem0  15806  prmlem1a  15807  divsfval  16201  mrisval  16284  ismri  16285  ismri2dad  16291  cidpropd  16364  plttr  16964  joinval  16999  meetval  17013  acsfiindd  17171  isnsgrp  17282  mgm2nsgrplem2  17400  sgrp2nmndlem3  17406  symgfix2  17830  pmtrdifellem4  17893  psgnunilem1  17907  psgnunilem5  17908  psgnunilem2  17909  psgnunilem3  17910  pmtrsn  17933  sylow1lem3  18009  sylow2alem2  18027  efgsfo  18146  ablfac1eulem  18465  ablfac1eu  18466  pgpfac1lem1  18467  pgpfac1lem5  18472  islbs  19070  lbsind  19074  lbspss  19076  lbspropd  19093  lspsnne1  19111  islbs2  19148  lbsacsbs  19150  lbsextlem1  19152  lbsextlem3  19154  lbsextlem4  19155  lbsextg  19156  nzrunit  19261  opsrtoslem2  19479  cply1coe0  19663  cply1coe0bi  19664  frlmlbs  20130  islindf  20145  islinds2  20146  islindf2  20147  lindfind  20149  lindsind  20150  lindfrn  20154  lindfmm  20160  lsslindf  20163  islindf4  20171  mdetunilem7  20418  mdetunilem8  20419  mdetunilem9  20420  maducoeval2  20440  pmatcollpw3fi1lem1  20585  fvmptnn04ifa  20649  fvmptnn04ifc  20651  fvmptnn04ifd  20652  chfacffsupp  20655  chfacfscmul0  20657  chfacfpmmul0  20661  elcls  20871  maxlp  20945  perfi  20953  ordtbaslem  20986  ordtval  20987  ordtbas2  20989  ordtopn1  20992  ordtopn2  20993  ordtcnv  20999  ordtrest  21000  ordtrest2lem  21001  ordtrest2  21002  pnfnei  21018  mnfnei  21019  isreg2  21175  ordthauslem  21181  cmpfi  21205  cmpfii  21206  bwth  21207  nconnsubb  21220  hausdiag  21442  txkgen  21449  kqdisj  21529  ordthmeolem  21598  fbfinnfr  21639  trfbas  21642  fbunfip  21667  fbasrn  21682  trfil3  21686  ufileu  21717  fin1aufil  21730  hausflim  21779  alexsubALTlem2  21846  alexsubALTlem3  21847  alexsubALTlem4  21848  ptcmplem2  21851  ptcmplem3  21852  stdbdbl  22316  iccntr  22618  reconnlem2  22624  iccpnfcnv  22737  xrhmeo  22739  lebnumlem1  22754  lebnumlem2  22755  lebnumlem3  22756  bcthlem4  23118  minveclem3b  23193  ivthlem2  23215  ivthlem3  23216  mbfmax  23410  mbfposr  23413  i1fd  23442  mbfi1fseqlem4  23479  itg2splitlem  23509  itg2monolem1  23511  itg2cnlem1  23522  dvne0  23768  lhop1lem  23770  deg1nn0clb  23844  dgrle  23993  coemulhi  24004  aaliou3lem9  24099  cos11  24273  logleb  24343  argrege0  24351  logdivle  24362  ellogdm  24379  cxple  24435  cxplt2  24438  cxple3  24441  isosctrlem1  24542  atandm  24597  atans2  24652  atantayl2  24659  eldmgm  24742  ftalem7  24799  isppw2  24835  musum  24911  dchrsum2  24987  bposlem1  25003  lgsmod  25042  lgsdir2lem2  25045  lgsdir2  25049  lgsne0  25054  lgsprme0  25058  gausslemma2dlem4  25088  lgsquadlem1  25099  2lgslem3  25123  2lgsoddprm  25135  rpvmasumlem  25170  padicabv  25313  ostth3  25321  ostth  25322  istrkgld  25352  axtgupdim2  25364  tglowdim2l  25539  axlowdimlem16  25831  axlowdim2  25834  axlowdim  25835  numedglnl  26033  usgredg2v  26113  lfuhgr1v0e  26140  cusgrfi  26348  vtxd0nedgb  26378  vtxduhgr0edgnel  26384  1loopgrnb0  26392  1hevtxdg0  26395  vtxdgoddnumeven  26443  wlkp1lem1  26564  wlkp1lem2  26565  wlkp1lem5  26568  crctcsh  26710  clwwlknclwwlkdifs  26867  clwlkclwwlklem2a4  26892  eupth2eucrct  27070  eupth2lem3lem3  27083  eupth2lem3lem4  27084  eupth2lem3lem6  27086  eupth2lem3lem7  27087  eupth2lems  27091  eupth2  27092  konigsberglem4  27110  nfrgr2v  27129  frgrwopreglem3  27169  fusgr2wsp2nb  27185  frgrreggt1  27235  friendshipgt3  27240  lpni  27316  nmobndseqi  27618  minvecolem5  27721  chpsscon3  28346  chnle  28357  nonbooli  28494  pjnel  28569  specval  28741  nmcfnlbi  28895  stri  29100  hstri  29108  cvbr  29125  cvcon3  29127  chcv1  29198  cvexchlem  29211  chrelat2  29213  spc2d  29297  elpreq  29344  ifeqeqx  29345  isoun  29464  suppss3  29487  xrge0infss  29510  infxrge0gelb  29516  eliccelico  29524  elicoelioo  29525  nndiffz1  29533  nn0min  29552  toslublem  29652  tosglblem  29654  isarchi2  29724  archiabl  29737  ordtcnvNEW  29951  ordtrestNEW  29952  ordtrest2NEWlem  29953  ordtrest2NEW  29954  ordtconnlem1  29955  xrge0iifcnv  29964  elzdif0  30009  esumpcvgval  30125  esum2d  30140  ddemeas  30284  omssubadd  30347  oddpwdc  30401  eulerpartlems  30407  eulerpartlemf  30417  eulerpartlemt  30418  eulerpartlemr  30421  eulerpartlemgvv  30423  eulerpartlemn  30428  ballotlemfc0  30539  ballotlemfcc  30540  ballotlem4  30545  ballotlemimin  30552  ballotlem7  30582  plymulx  30610  signsply0  30613  reprinfz1  30685  reprpmtf1o  30689  reprdifc  30690  hgt750lema  30720  hgt750leme  30721  istrkg2d  30729  bnj23  30769  bnj1185  30849  bnj1228  31064  bnj1388  31086  bnj1417  31094  erdszelem10  31167  ismfs  31431  mvtinf  31437  untelirr  31570  untsucf  31572  untangtr  31576  ceqsralv2  31593  inffzOLD  31601  dfpo2  31631  dfon2lem3  31674  dfon2lem4  31675  dfon2lem7  31678  dfon2lem9  31680  distel  31693  soseq  31735  noextenddif  31805  nodenselem4  31821  nodenselem5  31822  nodenselem7  31824  nolt02o  31829  noresle  31830  noprefixmo  31832  nosupdm  31834  nosupfv  31836  nosupres  31837  nosupbnd1lem1  31838  nosupbnd1lem3  31840  nosupbnd1lem5  31842  nosupbnd1  31844  nosupbnd2lem1  31845  nosupbnd2  31846  slenlt  31861  nocvxminlem  31877  slerec  31907  funpartfv  32036  dfrdg4  32042  nn0prpwlem  32301  nn0prpw  32302  limsucncmpi  32428  limsucncmp  32429  ordcmp  32430  unblimceq0  32482  unbdqndv1  32483  bj-hbntbi  32679  bj-cbvexdv  32720  bj-cbvex2v  32722  bj-drex1v  32733  bj-nalset  32778  bj-dtru  32781  bj-ru0  32916  bj-nuliota  33003  topdifinffinlem  33175  topdifinffin  33176  icorempt2  33179  relowlpssretop  33192  finxpreclem2  33207  finxpreclem6  33213  wl-ax11-lem8  33349  leceifl  33378  lindsenlbs  33384  matunitlindflem1  33385  poimirlem16  33405  poimirlem17  33406  poimirlem18  33407  poimirlem19  33408  poimirlem21  33410  poimirlem23  33412  poimirlem26  33415  poimirlem27  33416  poimirlem28  33417  poimirlem31  33420  poimir  33422  mblfinlem2  33427  mblfinlem3  33428  ismblfin  33430  cnambfre  33438  itg2addnclem  33441  itg2addnclem2  33442  iblabsnclem  33453  ftc1anclem1  33465  areacirc  33485  heibor1lem  33588  heiborlem1  33590  heiborlem6  33595  heiborlem8  33597  heiborlem10  33599  smprngopr  33831  ax12inda  34059  riotaclbgBAD  34066  lcvfbr  34133  lcvbr  34134  lsatcv0  34144  l1cvpat  34167  opltcon3b  34317  cvrfval  34381  cvrval  34382  cvrnbtwn  34384  cvrval2  34387  cvrnbtwn2  34388  cvrnbtwn3  34389  cvrcon3b  34390  cvrnbtwn4  34392  atnlt  34426  iscvlat  34436  cvlexch1  34441  hlsuprexch  34493  hlrelat5N  34513  hlrelat2  34515  cvrval5  34527  3dimlem1  34570  3dim1lem5  34578  3dim2  34580  3dim3  34581  llnnlt  34635  islpln5  34647  lplni2  34649  lvolex3N  34650  lplnnle2at  34653  islpln2a  34660  lplnribN  34663  lplnexllnN  34676  lplnnlt  34677  lvoli3  34689  islvol5  34691  lvoli2  34693  lvolnle3at  34694  islvol2aN  34704  4atlem11  34721  lvolnltN  34730  dalawlem15  34997  4atexlemex2  35183  4atex  35188  4atex2-0aOLDN  35190  4atex2-0cOLDN  35192  lautcvr  35204  ltrnfset  35229  ltrnset  35230  ltrnu  35233  trlfset  35273  trlset  35274  trlval2  35276  cdlemd6  35316  cdleme0nex  35403  cdleme18d  35408  cdleme25b  35468  cdleme25cv  35472  cdleme29b  35489  cdleme31fv  35504  cdleme31fv2  35507  cdlemefrs29bpre0  35510  cdlemefr32sn2aw  35518  cdlemefr29bpre0N  35520  cdlemefr29clN  35521  cdlemefr32fvaN  35523  cdlemefr32fva1  35524  cdlemefs32sn1aw  35528  cdleme32fva  35551  cdleme32fvaw  35553  cdleme40v  35583  cdleme42b  35592  cdleme46f2g2  35607  cdleme46f2g1  35608  cdleme48gfv  35651  cdlemg1fvawlemN  35687  cdlemg1cex  35702  cdlemg6d  35735  cdlemm10N  36233  dicffval  36289  dicfval  36290  dicval  36291  dicfnN  36298  dicvalrelN  36300  dihffval  36345  dihfval  36346  dihlsscpre  36349  dvh4dimat  36553  dvh3dimatN  36554  dvh4dimlem  36558  dvh3dim  36561  dvh4dimN  36562  dvh3dim2  36563  dvh3dim3N  36564  mapdcv  36775  mapdh9aOLDN  36906  hdmapfval  36945  hdmapval  36946  hdmapval2  36950  hdmap11lem2  36960  ellz1  37156  rencldnfilem  37210  jm2.22  37388  jm2.23  37389  wepwsolem  37438  fnwe2lem2  37447  aomclem8  37457  unxpwdom3  37491  ifpbi12  37659  ifpbi123  37661  relintabex  37713  ss2iundf  37777  frege124d  37879  clsk3nimkb  38164  clsk1indlem1  38169  clsk1independent  38170  ntrneineine1lem  38208  ntrneicls11  38214  clsneiel1  38232  clsneiel2  38233  neicvgel1  38243  neicvgel2  38244  radcnvrat  38339  rusbcALT  38466  en3lpVD  38906  eliin2f  39113  nssd  39114  wessf1ornlem  39193  limsupre2lem  39762  icccncfext  39869  stoweidlem14  40000  stoweidlem34  40020  stoweidlem59  40045  etransclem24  40244  nnfoctbdjlem  40441  nnfoctbdj  40442  hspmbllem2  40610  smfmbfcex  40737  nsssmfmbflem  40755  eu2ndop1stv  40971  afvfv0bi  41001  afvco2  41025  ndmaovg  41033  nelbr  41060  otiunsndisjX  41067  fun2dmnopgexmpl  41072  ltnltne  41082  fmtnoinf  41219  odz2prm2pw  41246  prmdvdsfmtnof1lem2  41268  lighneallem3  41295  lighneallem4  41298  isodd3  41336  bits0ALTV  41361  lidldomnnring  41701  zrninitoringc  41842  ztprmneprm  41896  lindepsnlininds  42012  islindeps  42013  lindslinindsimp2lem5  42022  lindslinindsimp2  42023  difmodm1lt  42088  elsetrecslem  42215
  Copyright terms: Public domain W3C validator