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 303 . . 3 (𝜓 ↔ ¬ ¬ 𝜓)
3 notnotb 303 . . 3 (𝜒 ↔ ¬ ¬ 𝜒)
41, 2, 33bitr3g 301 . 2 (𝜑 → (¬ ¬ 𝜓 ↔ ¬ ¬ 𝜒))
54con4bid 306 1 (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 195
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 196
This theorem is referenced by:  notbi  308  ifpbi123d  1021  con3ALT  1026  con3OLD  1029  nanbi1  1447  xorbi12d  1470  cbvexvw  1957  hba1wOLD  1962  hbe1w  1963  cbvexv1  2164  cbvex  2260  cbvexv  2263  cbvexd  2266  cbvex2  2268  cbvexdva  2271  drex1  2315  eujustALT  2461  necon3abid  2818  neleq12d  2887  cbvrexf  3142  gencbval  3225  spcegf  3262  spc2gv  3269  spc3gv  3271  cdeqnot  3390  ru  3401  sbcng  3443  sbcrext  3478  sbcrextOLD  3479  cbvrexcsf  3532  difjust  3542  eldif  3550  dfpss3  3655  difeq2  3684  disjne  3974  pssdifcom1  4006  eldifpr  4152  elpwunsn  4171  eldiftp  4175  prel12  4323  prel12g  4327  disjxun  4581  nalset  4723  pwnss  4756  dtru  4783  rexxfrd  4807  rexxfr2d  4809  rexxfrd2  4811  rexxfr  4814  dtruALT  4826  dtruALT2  4838  opthneg  4876  otiunsndisj  4905  poeq1  4962  pocl  4966  swopo  4969  sotric  4985  sotrieq  4986  isso2i  4991  somo  4993  freq1  5008  frirr  5015  fr2nr  5016  frminex  5018  tz7.2  5022  wereu2  5035  poinxp  5105  frinxp  5107  posn  5110  frsn  5112  rexiunxp  5184  rexxpf  5191  intirr  5433  poirr2  5439  cnvpo  5590  predpoirr  5625  predfrirr  5626  nordeq  5659  ordtri1  5673  ordtri3  5676  ordtri3OLD  5677  fvmpti  6190  fndmdif  6229  rexrnmpt  6277  f1imapss  6424  cbvexfo  6445  soisoi  6478  isopolem  6495  weniso  6504  canth  6508  riotaclb  6548  rexrnmpt2  6674  ndmovg  6715  sorpssuni  6844  sorpssint  6845  fr3nr  6871  dfwe2  6873  ordsucsssuc  6915  nlimsucg  6934  orduninsuc  6935  dfom2  6959  ssnlim  6975  f1oweALT  7043  frxp  7174  poxp  7176  wfrlem10  7311  smoword  7350  tz7.48lem  7423  oacan  7515  oaword  7516  omlimcl  7545  omeulem1  7549  nnaword  7594  nnmword  7600  nneob  7619  brdifun  7658  swoer  7659  undifixp  7830  boxcutc  7837  2dom  7915  php  8029  nndomo  8039  nnsdomo  8040  unxpdomlem2  8050  frfi  8090  unfilem1  8109  supeq3  8238  supeq123d  8239  supmo  8241  eqsup  8245  supub  8248  sup0  8255  suppr  8260  supisolem  8262  supisoex  8263  eqinf  8273  infval  8275  infmo  8284  infpr  8292  infempty  8295  oieq1  8300  ordtypecbv  8305  ordtypelem7  8312  wemapsolem  8338  canthwdom  8367  zfregcl  8382  zfregclOLD  8384  elirrv  8387  elirr  8388  noinfep  8440  cantnfp1lem3  8460  rankr1clem  8566  carden2b  8676  domtri2  8698  alephord3  8784  alephdom2  8793  alephval3  8816  dfac9  8841  kmlem2  8856  kmlem4  8858  isfin4  9002  isfin7  9006  fin23lem11  9022  isf32lem5  9062  isf34lem4  9082  fin1a2lem6  9110  fin1a2lem7  9111  fin1a2lem12  9116  itunisuc  9124  ac6n  9190  zorn2g  9208  zornn0g  9210  ttukeylem7  9220  axpowndlem3  9300  axpowndlem4  9301  axregnd  9305  elgch  9323  engch  9329  fpwwe2lem13  9343  fpwwe2  9344  pwfseqlem1  9359  pwfseqlem3  9361  hargch  9374  addnidpi  9602  pinq  9628  nqereu  9630  ltsonq  9670  prlem934  9734  ltexprlem7  9743  addcanpr  9747  prlem936  9748  reclem2pr  9749  reclem3pr  9750  supexpr  9755  ltsosr  9794  supsrlem  9811  axpre-lttri  9865  axpre-sup  9869  xrlenlt  9982  axlttri  9988  axsup  9992  ltne  10013  dedekind  10079  readdcan  10089  leadd1  10375  ltsub1  10403  ltsub2  10404  leord1  10434  lediv1  10767  lemuldiv  10782  lerec  10785  le2msq  10802  lbinf  10855  infm3  10861  suprnub  10865  infregelb  10884  avgle1  11149  avgle2  11150  znnnlt1  11281  indstr  11632  zsupss  11653  uzsupss  11656  rpneg  11739  xralrple  11910  xleneg  11923  xltadd1  11958  xposdif  11964  xmulneg1  11971  xltmul1  11994  xrsupexmnf  12007  xrinfmexpnf  12008  xrsupsslem  12009  xrinfmsslem  12010  xrub  12014  supxrleub  12028  infxrgelb  12037  difreicc  12175  nn0disj  12324  nelfzo  12344  elfznelfzo  12439  fvinim0ffz  12449  injresinjlem  12450  ssnn0fi  12646  leexp2  12777  hashbnd  12985  hasheni  12998  hashbc  13094  wrdsymb0  13194  swrdnd  13284  swrdnd2  13285  repswswrd  13382  repswccat  13383  cshwidxmod  13400  cnpart  13828  sqrtlt  13850  limsuplt  14058  rlimrege0  14158  isercoll  14246  efle  14687  odd2np1  14903  sumodd  14949  divalglem7  14960  ndvdsadd  14972  fldivndvdslt  14976  bitsfval  14983  bitsval  14984  bits0  14988  bitsp1  14991  bitsmod  14996  bitscmp  14998  bitsinv1lem  15001  sadadd2lem2  15010  saddisjlem  15024  bitsshft  15035  gcdneg  15081  algcvgblem  15128  lcmneg  15154  isprm3  15234  dvdsnprmd  15241  isprm5  15257  rpexp  15270  phiprmpw  15319  m1dvdsndvds  15341  pythagtrip  15377  pcgcd1  15419  prmpwdvds  15446  prmreclem2  15459  prmreclem3  15460  prmreclem5  15462  prmreclem6  15463  vdwlem6  15528  vdwnnlem2  15538  vdwnnlem3  15539  vdwnn  15540  prmo1  15579  prmlem0  15650  prmlem1a  15651  divsfval  16030  mrisval  16113  ismri  16114  ismri2dad  16120  cidpropd  16193  plttr  16793  joinval  16828  meetval  16842  acsfiindd  17000  isnsgrp  17111  mgm2nsgrplem2  17229  sgrp2nmndlem3  17235  symgfix2  17659  pmtrdifellem4  17722  psgnunilem1  17736  psgnunilem5  17737  psgnunilem2  17738  psgnunilem3  17739  pmtrsn  17762  sylow1lem3  17838  sylow2alem2  17856  efgsfo  17975  ablfac1eulem  18294  ablfac1eu  18295  pgpfac1lem1  18296  pgpfac1lem5  18301  islbs  18897  lbsind  18901  lbspss  18903  lbspropd  18920  lspsnne1  18938  islbs2  18975  lbsacsbs  18977  lbsextlem1  18979  lbsextlem3  18981  lbsextlem4  18982  lbsextg  18983  nzrunit  19088  opsrtoslem2  19306  cply1coe0  19490  cply1coe0bi  19491  frlmlbs  19955  islindf  19970  islinds2  19971  islindf2  19972  lindfind  19974  lindsind  19975  lindfrn  19979  lindfmm  19985  lsslindf  19988  islindf4  19996  mdetunilem7  20243  mdetunilem8  20244  mdetunilem9  20245  maducoeval2  20265  pmatcollpw3fi1lem1  20410  fvmptnn04ifa  20474  fvmptnn04ifc  20476  fvmptnn04ifd  20477  chfacffsupp  20480  chfacfscmul0  20482  chfacfpmmul0  20486  elcls  20687  maxlp  20761  perfi  20769  ordtbaslem  20802  ordtval  20803  ordtbas2  20805  ordtopn1  20808  ordtopn2  20809  ordtcnv  20815  ordtrest  20816  ordtrest2lem  20817  ordtrest2  20818  pnfnei  20834  mnfnei  20835  isreg2  20991  ordthauslem  20997  cmpfi  21021  cmpfii  21022  bwth  21023  nconsubb  21036  hausdiag  21258  txkgen  21265  kqdisj  21345  ordthmeolem  21414  fbfinnfr  21455  trfbas  21458  fbunfip  21483  fbasrn  21498  trfil3  21502  ufileu  21533  fin1aufil  21546  hausflim  21595  alexsubALTlem2  21662  alexsubALTlem3  21663  alexsubALTlem4  21664  ptcmplem2  21667  ptcmplem3  21668  stdbdbl  22132  iccntr  22432  reconnlem2  22438  iccpnfcnv  22551  xrhmeo  22553  lebnumlem1  22568  lebnumlem2  22569  lebnumlem3  22570  bcthlem4  22932  minveclem3b  23007  ivthlem2  23028  ivthlem3  23029  mbfmax  23222  mbfposr  23225  i1fd  23254  mbfi1fseqlem4  23291  itg2splitlem  23321  itg2monolem1  23323  itg2cnlem1  23334  dvne0  23578  lhop1lem  23580  deg1nn0clb  23654  dgrle  23803  coemulhi  23814  aaliou3lem9  23909  cos11  24083  logleb  24153  argrege0  24161  logdivle  24172  ellogdm  24185  cxple  24241  cxplt2  24244  cxple3  24247  isosctrlem1  24348  atandm  24403  atans2  24458  atantayl2  24465  eldmgm  24548  ftalem7  24605  isppw2  24641  musum  24717  dchrsum2  24793  bposlem1  24809  lgsmod  24848  lgsdir2lem2  24851  lgsdir2  24855  lgsne0  24860  lgsprme0  24864  gausslemma2dlem4  24894  lgsquadlem1  24905  2lgslem3  24929  2lgsoddprm  24941  rpvmasumlem  24976  padicabv  25119  ostth3  25127  ostth  25128  istrkgld  25158  axtgupdim2  25170  tglowdim2l  25345  axlowdimlem16  25637  axlowdim2  25640  axlowdim  25641  usgra1v  25919  usgraidx2v  25922  nbgra0nb  25958  cusgrafilem3  26009  spthispth  26103  wlkdvspthlem  26137  clwlkisclwwlklem2a4  26312  clwlknclwlkdifs  26487  eupath2lem3  26506  eupath2  26507  konigsberg  26514  frgra2v  26526  frgrancvvdeqlem2  26558  2spotiundisj  26589  usg2spot2nb  26592  2spotmdisj  26595  frgrareggt1  26643  friendshipgt3  26648  lpni  26722  nmobndseqi  27018  minvecolem5  27121  chpsscon3  27746  chnle  27757  nonbooli  27894  pjnel  27969  specval  28141  nmcfnlbi  28295  stri  28500  hstri  28508  cvbr  28525  cvcon3  28527  chcv1  28598  cvexchlem  28611  chrelat2  28613  spc2d  28697  elpreq  28744  ifeqeqx  28745  isoun  28862  suppss3  28890  xrge0infss  28915  infxrge0gelb  28921  eliccelico  28929  elicoelioo  28930  nndiffz1  28936  nn0min  28954  toslublem  28998  tosglblem  29000  isarchi2  29070  archiabl  29083  ordtcnvNEW  29294  ordtrestNEW  29295  ordtrest2NEWlem  29296  ordtrest2NEW  29297  ordtconlem1  29298  xrge0iifcnv  29307  elzdif0  29352  esumpcvgval  29467  esum2d  29482  ddemeas  29626  omssubadd  29689  oddpwdc  29743  eulerpartlems  29749  eulerpartlemf  29759  eulerpartlemt  29760  eulerpartlemr  29763  eulerpartlemgvv  29765  eulerpartlemn  29770  ballotlemfc0  29881  ballotlemfcc  29882  ballotlem4  29887  ballotlemimin  29894  ballotlem7  29924  plymulx  29951  signsply0  29954  istrkg2d  29997  bnj23  30038  bnj1185  30118  bnj1228  30333  bnj1388  30355  bnj1417  30363  erdszelem10  30436  ismfs  30700  mvtinf  30706  untelirr  30839  untsucf  30841  untangtr  30845  ceqsralv2  30862  inffzOLD  30868  dfpo2  30898  dfon2lem3  30934  dfon2lem4  30935  dfon2lem7  30938  dfon2lem9  30940  distel  30953  soseq  30995  nodenselem4  31083  nodenselem5  31084  nocvxminlem  31089  nofulllem4  31104  funpartfv  31222  dfrdg4  31228  nn0prpwlem  31487  nn0prpw  31488  limsucncmpi  31614  limsucncmp  31615  ordcmp  31616  unblimceq0  31668  unbdqndv1  31669  bj-hbntbi  31882  bj-cbvexdv  31923  bj-cbvex2v  31925  bj-drex1v  31937  bj-nalset  31982  bj-dtru  31985  bj-ru0  32124  bj-nuliota  32210  topdifinffinlem  32371  topdifinffin  32372  icorempt2  32375  relowlpssretop  32388  finxpreclem2  32403  finxpreclem6  32409  wl-ax11-lem8  32548  leceifl  32568  lindsenlbs  32574  matunitlindflem1  32575  poimirlem16  32595  poimirlem17  32596  poimirlem18  32597  poimirlem19  32598  poimirlem21  32600  poimirlem23  32602  poimirlem26  32605  poimirlem27  32606  poimirlem28  32607  poimirlem31  32610  poimir  32612  mblfinlem2  32617  mblfinlem3  32618  ismblfin  32620  cnambfre  32628  itg2addnclem  32631  itg2addnclem2  32632  iblabsnclem  32643  ftc1anclem1  32655  areacirc  32675  heibor1lem  32778  heiborlem1  32780  heiborlem6  32785  heiborlem8  32787  heiborlem10  32789  smprngopr  33021  ax12inda  33251  riotaclbgBAD  33258  lcvfbr  33325  lcvbr  33326  lsatcv0  33336  l1cvpat  33359  opltcon3b  33509  cvrfval  33573  cvrval  33574  cvrnbtwn  33576  cvrval2  33579  cvrnbtwn2  33580  cvrnbtwn3  33581  cvrcon3b  33582  cvrnbtwn4  33584  atnlt  33618  iscvlat  33628  cvlexch1  33633  hlsuprexch  33685  hlrelat5N  33705  hlrelat2  33707  cvrval5  33719  3dimlem1  33762  3dim1lem5  33770  3dim2  33772  3dim3  33773  llnnlt  33827  islpln5  33839  lplni2  33841  lvolex3N  33842  lplnnle2at  33845  islpln2a  33852  lplnribN  33855  lplnexllnN  33868  lplnnlt  33869  lvoli3  33881  islvol5  33883  lvoli2  33885  lvolnle3at  33886  islvol2aN  33896  4atlem11  33913  lvolnltN  33922  dalawlem15  34189  4atexlemex2  34375  4atex  34380  4atex2-0aOLDN  34382  4atex2-0cOLDN  34384  lautcvr  34396  ltrnfset  34421  ltrnset  34422  ltrnu  34425  trlfset  34465  trlset  34466  trlval2  34468  cdlemd6  34508  cdleme0nex  34595  cdleme18d  34600  cdleme25b  34660  cdleme25cv  34664  cdleme29b  34681  cdleme31fv  34696  cdleme31fv2  34699  cdlemefrs29bpre0  34702  cdlemefr32sn2aw  34710  cdlemefr29bpre0N  34712  cdlemefr29clN  34713  cdlemefr32fvaN  34715  cdlemefr32fva1  34716  cdlemefs32sn1aw  34720  cdleme32fva  34743  cdleme32fvaw  34745  cdleme40v  34775  cdleme42b  34784  cdleme46f2g2  34799  cdleme46f2g1  34800  cdleme48gfv  34843  cdlemg1fvawlemN  34879  cdlemg1cex  34894  cdlemg6d  34927  cdlemm10N  35425  dicffval  35481  dicfval  35482  dicval  35483  dicfnN  35490  dicvalrelN  35492  dihffval  35537  dihfval  35538  dihlsscpre  35541  dvh4dimat  35745  dvh3dimatN  35746  dvh4dimlem  35750  dvh3dim  35753  dvh4dimN  35754  dvh3dim2  35755  dvh3dim3N  35756  mapdcv  35967  mapdh9aOLDN  36098  hdmapfval  36137  hdmapval  36138  hdmapval2  36142  hdmap11lem2  36152  ellz1  36348  rencldnfilem  36402  jm2.22  36580  jm2.23  36581  wepwsolem  36630  fnwe2lem2  36639  aomclem8  36649  unxpwdom3  36683  ifpbi12  36852  ifpbi123  36854  relintabex  36906  ss2iundf  36970  frege124d  37072  clsk3nimkb  37358  clsk1indlem1  37363  clsk1independent  37364  ntrneineine1lem  37402  ntrneicls11  37408  clsneiel1  37426  clsneiel2  37427  neicvgel1  37437  neicvgel2  37438  radcnvrat  37535  rusbcALT  37662  en3lpVD  38102  eliin2f  38316  nssd  38317  wessf1ornlem  38366  icccncfext  38773  stoweidlem14  38907  stoweidlem34  38927  stoweidlem59  38952  etransclem24  39151  nnfoctbdjlem  39348  nnfoctbdj  39349  hspmbllem2  39517  smfmbfcex  39646  nsssmfmbflem  39664  eu2ndop1stv  39851  afvfv0bi  39881  afvco2  39905  ndmaovg  39913  fmtnoinf  39986  odz2prm2pw  40013  prmdvdsfmtnof1lem2  40035  lighneallem3  40062  lighneallem4  40065  isodd3  40103  bits0ALTV  40128  otiunsndisjX  40317  2f1fvneq  40322  fun2dmnopgexmpl  40329  ltnltne  40345  usgredg2v  40454  lfuhgr1v0e  40480  cusgrfi  40674  vtxd0nedgb  40703  vtxduhgr0edgnel  40709  1loopgrnb0  40717  1hevtxdg0  40720  1wlkp1lem1  40882  1wlkp1lem2  40883  1wlkp1lem5  40886  crctcsh  41027  clwwlknclwwlkdifs  41181  clwlkclwwlklem2a4  41206  eupth2eucrct  41385  eupth2lem3lem3  41398  eupth2lem3lem4  41399  eupth2lem3lem6  41401  eupth2lem3lem7  41402  eupth2lems  41406  eupth2  41407  konigsberglem4  41425  nfrgr2v  41442  frgrncvvdeqlem2  41470  fusgr2wsp2nb  41498  av-frgrareggt1  41547  av-friendshipgt3  41552  lidldomnnring  41720  zrninitoringc  41863  ztprmneprm  41918  lindepsnlininds  42035  islindeps  42036  lindslinindsimp2lem5  42045  lindslinindsimp2  42046  difmodm1lt  42111  elsetrecslem  42243
  Copyright terms: Public domain W3C validator