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

Theorem notbid 306
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 302 . . 3 (𝜓 ↔ ¬ ¬ 𝜓)
3 notnotb 302 . . 3 (𝜒 ↔ ¬ ¬ 𝜒)
41, 2, 33bitr3g 300 . 2 (𝜑 → (¬ ¬ 𝜓 ↔ ¬ ¬ 𝜒))
54con4bid 305 1 (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194
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 195
This theorem is referenced by:  notbi  307  ifpbi123d  1020  con3ALT  1025  con3OLD  1028  nanbi1  1446  xorbi12d  1469  cbvexvw  1956  hba1wOLD  1961  hbe1w  1962  cbvexv1  2162  cbvex  2258  cbvexv  2261  cbvexd  2264  cbvex2  2266  cbvexdva  2269  drex1  2314  eujustALT  2460  necon3abid  2817  neleq12d  2886  cbvrexf  3141  gencbval  3224  spcegf  3261  spc2gv  3268  spc3gv  3270  cdeqnot  3389  ru  3400  sbcng  3442  sbcrext  3477  sbcrextOLD  3478  cbvrexcsf  3531  difjust  3541  eldif  3549  dfpss3  3654  difeq2  3683  disjne  3973  pssdifcom1  4005  eldifpr  4151  elpwunsn  4170  eldiftp  4174  prel12  4318  prel12g  4322  disjxun  4575  nalset  4718  pwnss  4751  dtru  4778  rexxfrd  4802  rexxfr2d  4804  rexxfrd2  4806  rexxfr  4809  dtruALT  4821  dtruALT2  4833  opthneg  4870  otiunsndisj  4896  poeq1  4952  pocl  4956  swopo  4959  sotric  4975  sotrieq  4976  isso2i  4981  somo  4983  freq1  4998  frirr  5005  fr2nr  5006  frminex  5008  tz7.2  5012  wereu2  5025  poinxp  5095  frinxp  5097  posn  5100  frsn  5102  rexiunxp  5172  rexxpf  5179  intirr  5420  poirr2  5426  cnvpo  5576  predpoirr  5611  predfrirr  5612  nordeq  5645  ordtri1  5659  ordtri3  5662  ordtri3OLD  5663  fvmpti  6175  fndmdif  6214  rexrnmpt  6262  f1imapss  6402  cbvexfo  6423  soisoi  6456  isopolem  6473  weniso  6482  canth  6486  riotaclb  6526  rexrnmpt2  6652  ndmovg  6692  sorpssuni  6821  sorpssint  6822  fr3nr  6848  dfwe2  6850  ordsucsssuc  6892  nlimsucg  6911  orduninsuc  6912  dfom2  6936  ssnlim  6952  f1oweALT  7020  frxp  7151  poxp  7153  wfrlem10  7288  smoword  7327  tz7.48lem  7400  oacan  7492  oaword  7493  omlimcl  7522  omeulem1  7526  nnaword  7571  nnmword  7577  nneob  7596  brdifun  7635  swoer  7636  undifixp  7807  boxcutc  7814  2dom  7892  php  8006  nndomo  8016  nnsdomo  8017  unxpdomlem2  8027  frfi  8067  unfilem1  8086  supeq3  8215  supeq123d  8216  supmo  8218  eqsup  8222  supub  8225  sup0  8232  suppr  8237  supisolem  8239  supisoex  8240  eqinf  8250  infval  8252  infmo  8261  infpr  8269  infempty  8272  oieq1  8277  ordtypecbv  8282  ordtypelem7  8289  wemapsolem  8315  canthwdom  8344  zfregcl  8359  zfregclOLD  8361  elirrv  8364  elirr  8365  noinfep  8417  cantnfp1lem3  8437  rankr1clem  8543  carden2b  8653  domtri2  8675  alephord3  8761  alephdom2  8770  alephval3  8793  dfac9  8818  kmlem2  8833  kmlem4  8835  isfin4  8979  isfin7  8983  fin23lem11  8999  isf32lem5  9039  isf34lem4  9059  fin1a2lem6  9087  fin1a2lem7  9088  fin1a2lem12  9093  itunisuc  9101  ac6n  9167  zorn2g  9185  zornn0g  9187  ttukeylem7  9197  axpowndlem3  9277  axpowndlem4  9278  axregnd  9282  elgch  9300  engch  9306  fpwwe2lem13  9320  fpwwe2  9321  pwfseqlem1  9336  pwfseqlem3  9338  hargch  9351  addnidpi  9579  pinq  9605  nqereu  9607  ltsonq  9647  prlem934  9711  ltexprlem7  9720  addcanpr  9724  prlem936  9725  reclem2pr  9726  reclem3pr  9727  supexpr  9732  ltsosr  9771  supsrlem  9788  axpre-lttri  9842  axpre-sup  9846  xrlenlt  9954  axlttri  9960  axsup  9964  ltne  9985  dedekind  10051  readdcan  10061  leadd1  10345  ltsub1  10373  ltsub2  10374  leord1  10404  lediv1  10737  lemuldiv  10752  lerec  10755  le2msq  10772  lbinf  10825  infm3  10831  suprnub  10835  infregelb  10854  avgle1  11119  avgle2  11120  znnnlt1  11237  indstr  11588  zsupss  11609  uzsupss  11612  rpneg  11695  xralrple  11869  xleneg  11882  xltadd1  11915  xposdif  11921  xmulneg1  11928  xltmul1  11951  xrsupexmnf  11963  xrinfmexpnf  11964  xrsupsslem  11965  xrinfmsslem  11966  xrub  11970  supxrleub  11984  infxrgelb  11993  difreicc  12131  nn0disj  12279  nelfzo  12299  elfznelfzo  12394  fvinim0ffz  12404  injresinjlem  12405  ssnn0fi  12601  leexp2  12732  hashbnd  12940  hasheni  12950  hashbc  13046  wrdsymb0  13140  swrdnd  13230  swrdnd2  13231  repswswrd  13328  repswccat  13329  cshwidxmod  13346  cnpart  13774  sqrtlt  13796  limsuplt  14004  rlimrege0  14104  isercoll  14192  efle  14633  odd2np1  14849  sumodd  14895  divalglem7  14906  ndvdsadd  14918  fldivndvdslt  14922  bitsfval  14929  bitsval  14930  bits0  14934  bitsp1  14937  bitsmod  14942  bitscmp  14944  bitsinv1lem  14947  sadadd2lem2  14956  saddisjlem  14970  bitsshft  14981  gcdneg  15027  algcvgblem  15074  lcmneg  15100  isprm3  15180  dvdsnprmd  15187  isprm5  15203  rpexp  15216  phiprmpw  15265  m1dvdsndvds  15287  pythagtrip  15323  pcgcd1  15365  prmpwdvds  15392  prmreclem2  15405  prmreclem3  15406  prmreclem5  15408  prmreclem6  15409  vdwlem6  15474  vdwnnlem2  15484  vdwnnlem3  15485  vdwnn  15486  prmo1  15525  prmlem0  15596  prmlem1a  15597  divsfval  15976  mrisval  16059  ismri  16060  ismri2dad  16066  cidpropd  16139  plttr  16739  joinval  16774  meetval  16788  acsfiindd  16946  isnsgrp  17057  mgm2nsgrplem2  17175  sgrp2nmndlem3  17181  symgfix2  17605  pmtrdifellem4  17668  psgnunilem1  17682  psgnunilem5  17683  psgnunilem2  17684  psgnunilem3  17685  pmtrsn  17708  sylow1lem3  17784  sylow2alem2  17802  efgsfo  17921  ablfac1eulem  18240  ablfac1eu  18241  pgpfac1lem1  18242  pgpfac1lem5  18247  islbs  18843  lbsind  18847  lbspss  18849  lbspropd  18866  lspsnne1  18884  islbs2  18921  lbsacsbs  18923  lbsextlem1  18925  lbsextlem3  18927  lbsextlem4  18928  lbsextg  18929  nzrunit  19034  opsrtoslem2  19252  cply1coe0  19436  cply1coe0bi  19437  frlmlbs  19897  islindf  19912  islinds2  19913  islindf2  19914  lindfind  19916  lindsind  19917  lindfrn  19921  lindfmm  19927  lsslindf  19930  islindf4  19938  mdetunilem7  20185  mdetunilem8  20186  mdetunilem9  20187  maducoeval2  20207  pmatcollpw3fi1lem1  20352  fvmptnn04ifa  20416  fvmptnn04ifc  20418  fvmptnn04ifd  20419  chfacffsupp  20422  chfacfscmul0  20424  chfacfpmmul0  20428  elcls  20629  maxlp  20703  perfi  20711  ordtbaslem  20744  ordtval  20745  ordtbas2  20747  ordtopn1  20750  ordtopn2  20751  ordtcnv  20757  ordtrest  20758  ordtrest2lem  20759  ordtrest2  20760  pnfnei  20776  mnfnei  20777  isreg2  20933  ordthauslem  20939  cmpfi  20963  cmpfii  20964  bwth  20965  nconsubb  20978  hausdiag  21200  txkgen  21207  kqdisj  21287  ordthmeolem  21356  fbfinnfr  21397  trfbas  21400  fbunfip  21425  fbasrn  21440  trfil3  21444  ufileu  21475  fin1aufil  21488  hausflim  21537  alexsubALTlem2  21604  alexsubALTlem3  21605  alexsubALTlem4  21606  ptcmplem2  21609  ptcmplem3  21610  stdbdbl  22073  iccntr  22364  reconnlem2  22370  iccpnfcnv  22482  xrhmeo  22484  lebnumlem1  22499  lebnumlem2  22500  lebnumlem3  22501  bcthlem4  22849  minveclem3b  22924  ivthlem2  22945  ivthlem3  22946  mbfmax  23139  mbfposr  23142  i1fd  23171  mbfi1fseqlem4  23208  itg2splitlem  23238  itg2monolem1  23240  itg2cnlem1  23251  dvne0  23495  lhop1lem  23497  deg1nn0clb  23571  dgrle  23720  coemulhi  23731  aaliou3lem9  23826  cos11  24000  logleb  24070  argrege0  24078  logdivle  24089  ellogdm  24102  cxple  24158  cxplt2  24161  cxple3  24164  isosctrlem1  24265  atandm  24320  atans2  24375  atantayl2  24382  eldmgm  24465  ftalem7  24522  isppw2  24558  musum  24634  dchrsum2  24710  bposlem1  24726  lgsmod  24765  lgsdir2lem2  24768  lgsdir2  24772  lgsne0  24777  lgsprme0  24781  gausslemma2dlem4  24811  lgsquadlem1  24822  2lgslem3  24846  2lgsoddprm  24858  rpvmasumlem  24893  padicabv  25036  ostth3  25044  ostth  25045  istrkgld  25075  axtgupdim2  25087  tglowdim2l  25263  axlowdimlem16  25555  axlowdim2  25558  axlowdim  25559  usgra1v  25685  usgraidx2v  25688  nbgra0nb  25724  cusgrafilem3  25775  spthispth  25869  wlkdvspthlem  25903  clwlkisclwwlklem2a4  26078  clwlknclwlkdifs  26253  eupath2lem3  26272  eupath2  26273  konigsberg  26280  frgra2v  26292  frgrancvvdeqlem2  26324  2spotiundisj  26355  usg2spot2nb  26358  2spotmdisj  26361  frgrareggt1  26409  friendshipgt3  26414  lpni  26488  nmobndseqi  26824  minvecolem5  26927  chpsscon3  27552  chnle  27563  nonbooli  27700  pjnel  27775  specval  27947  nmcfnlbi  28101  stri  28306  hstri  28314  cvbr  28331  cvcon3  28333  chcv1  28404  cvexchlem  28417  chrelat2  28419  spc2d  28503  elpreq  28550  ifeqeqx  28551  isoun  28668  suppss3  28696  xrge0infss  28721  infxrge0gelb  28727  eliccelico  28735  elicoelioo  28736  nndiffz1  28742  nn0min  28760  toslublem  28804  tosglblem  28806  isarchi2  28876  archiabl  28889  ordtcnvNEW  29100  ordtrestNEW  29101  ordtrest2NEWlem  29102  ordtrest2NEW  29103  ordtconlem1  29104  xrge0iifcnv  29113  elzdif0  29158  esumpcvgval  29273  esum2d  29288  ddemeas  29432  omssubadd  29495  oddpwdc  29549  eulerpartlems  29555  eulerpartlemf  29565  eulerpartlemt  29566  eulerpartlemr  29569  eulerpartlemgvv  29571  eulerpartlemn  29576  ballotlemfc0  29687  ballotlemfcc  29688  ballotlem4  29693  ballotlemimin  29700  ballotlem7  29730  plymulx  29757  signsply0  29760  istrkg2d  29803  bnj23  29844  bnj1185  29924  bnj1228  30139  bnj1388  30161  bnj1417  30169  erdszelem10  30242  ismfs  30506  mvtinf  30512  untelirr  30645  untsucf  30647  untangtr  30651  ceqsralv2  30668  inffzOLD  30674  dfpo2  30704  dfon2lem3  30740  dfon2lem4  30741  dfon2lem7  30744  dfon2lem9  30746  distel  30759  soseq  30801  nodenselem4  30889  nodenselem5  30890  nocvxminlem  30895  nofulllem4  30910  funpartfv  31028  dfrdg4  31034  nn0prpwlem  31293  nn0prpw  31294  limsucncmpi  31420  limsucncmp  31421  ordcmp  31422  unblimceq0  31474  unbdqndv1  31475  bj-hbntbi  31688  bj-cbvexdv  31729  bj-cbvex2v  31731  bj-drex1v  31744  bj-nalset  31795  bj-dtru  31798  bj-ru0  31927  bj-nuliota  32013  topdifinffinlem  32174  topdifinffin  32175  icorempt2  32178  relowlpssretop  32191  finxpreclem2  32206  finxpreclem6  32212  wl-ax11-lem8  32351  leceifl  32371  lindsenlbs  32377  matunitlindflem1  32378  poimirlem16  32398  poimirlem17  32399  poimirlem18  32400  poimirlem19  32401  poimirlem21  32403  poimirlem23  32405  poimirlem26  32408  poimirlem27  32409  poimirlem28  32410  poimirlem31  32413  poimir  32415  mblfinlem2  32420  mblfinlem3  32421  ismblfin  32423  cnambfre  32431  itg2addnclem  32434  itg2addnclem2  32435  iblabsnclem  32446  ftc1anclem1  32458  areacirc  32478  heibor1lem  32581  heiborlem1  32583  heiborlem6  32588  heiborlem8  32590  heiborlem10  32592  smprngopr  32824  ax12inda  33054  riotaclbgBAD  33061  lcvfbr  33128  lcvbr  33129  lsatcv0  33139  l1cvpat  33162  opltcon3b  33312  cvrfval  33376  cvrval  33377  cvrnbtwn  33379  cvrval2  33382  cvrnbtwn2  33383  cvrnbtwn3  33384  cvrcon3b  33385  cvrnbtwn4  33387  atnlt  33421  iscvlat  33431  cvlexch1  33436  hlsuprexch  33488  hlrelat5N  33508  hlrelat2  33510  cvrval5  33522  3dimlem1  33565  3dim1lem5  33573  3dim2  33575  3dim3  33576  llnnlt  33630  islpln5  33642  lplni2  33644  lvolex3N  33645  lplnnle2at  33648  islpln2a  33655  lplnribN  33658  lplnexllnN  33671  lplnnlt  33672  lvoli3  33684  islvol5  33686  lvoli2  33688  lvolnle3at  33689  islvol2aN  33699  4atlem11  33716  lvolnltN  33725  dalawlem15  33992  4atexlemex2  34178  4atex  34183  4atex2-0aOLDN  34185  4atex2-0cOLDN  34187  lautcvr  34199  ltrnfset  34224  ltrnset  34225  ltrnu  34228  trlfset  34268  trlset  34269  trlval2  34271  cdlemd6  34311  cdleme0nex  34398  cdleme18d  34403  cdleme25b  34463  cdleme25cv  34467  cdleme29b  34484  cdleme31fv  34499  cdleme31fv2  34502  cdlemefrs29bpre0  34505  cdlemefr32sn2aw  34513  cdlemefr29bpre0N  34515  cdlemefr29clN  34516  cdlemefr32fvaN  34518  cdlemefr32fva1  34519  cdlemefs32sn1aw  34523  cdleme32fva  34546  cdleme32fvaw  34548  cdleme40v  34578  cdleme42b  34587  cdleme46f2g2  34602  cdleme46f2g1  34603  cdleme48gfv  34646  cdlemg1fvawlemN  34682  cdlemg1cex  34697  cdlemg6d  34730  cdlemm10N  35228  dicffval  35284  dicfval  35285  dicval  35286  dicfnN  35293  dicvalrelN  35295  dihffval  35340  dihfval  35341  dihlsscpre  35344  dvh4dimat  35548  dvh3dimatN  35549  dvh4dimlem  35553  dvh3dim  35556  dvh4dimN  35557  dvh3dim2  35558  dvh3dim3N  35559  mapdcv  35770  mapdh9aOLDN  35901  hdmapfval  35940  hdmapval  35941  hdmapval2  35945  hdmap11lem2  35955  ellz1  36151  rencldnfilem  36205  jm2.22  36383  jm2.23  36384  wepwsolem  36433  fnwe2lem2  36442  aomclem8  36452  unxpwdom3  36486  ifpbi12  36655  ifpbi123  36657  relintabex  36709  ss2iundf  36773  frege124d  36875  clsk3nimkb  37161  clsk1indlem1  37166  clsk1independent  37167  ntrneineine1lem  37205  ntrneicls11  37211  clsneiel1  37229  clsneiel2  37230  neicvgel1  37240  neicvgel2  37241  radcnvrat  37338  rusbcALT  37465  en3lpVD  37905  eliin2f  38119  nssd  38120  wessf1ornlem  38169  icccncfext  38577  stoweidlem14  38711  stoweidlem34  38731  stoweidlem59  38756  etransclem24  38955  nnfoctbdjlem  39152  nnfoctbdj  39153  hspmbllem2  39321  smfmbfcex  39450  nsssmfmbflem  39468  eu2ndop1stv  39655  afvfv0bi  39686  afvco2  39710  ndmaovg  39718  fmtnoinf  39791  odz2prm2pw  39818  prmdvdsfmtnof1lem2  39840  lighneallem3  39867  lighneallem4  39870  isodd3  39908  bits0ALTV  39933  otiunsndisjX  40132  2f1fvneq  40138  fun2dmnopgexmpl  40156  ltnltne  40172  usgredg2v  40456  lfuhgr1v0e  40482  cusgrfi  40676  vtxd0nedgb  40705  vtxduhgr0edgnel  40711  1loopgrnb0  40719  1hevtxdg0  40722  1wlkp1lem1  40884  1wlkp1lem2  40885  1wlkp1lem5  40888  crctcsh  41029  clwwlknclwwlkdifs  41183  clwlkclwwlklem2a4  41208  eupth2eucrct  41387  eupth2lem3lem3  41400  eupth2lem3lem4  41401  eupth2lem3lem6  41403  eupth2lem3lem7  41404  eupth2lems  41408  eupth2  41409  konigsberglem4  41427  nfrgr2v  41444  frgrncvvdeqlem2  41472  fusgr2wsp2nb  41500  av-frgrareggt1  41549  av-friendshipgt3  41554  lidldomnnring  41722  zrninitoringc  41865  ztprmneprm  41920  lindepsnlininds  42037  islindeps  42038  lindslinindsimp2lem5  42047  lindslinindsimp2  42048  difmodm1lt  42113
  Copyright terms: Public domain W3C validator