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  2354  cbvex2v  2357  drex1v  2381  cbvex  2411  cbvexvOLD  2415  cbvex2  2428  drex1  2458  eujustALT  2653  necon3abid  3052  neleq12d  3127  cbvrexfw  3439  cbvrexf  3441  cbvrexdva2OLD  3459  gencbval  3552  spcegf  3591  spc2gv  3600  spc2d  3602  spc3gv  3604  cdeqnot  3758  rru  3769  ru  3770  sbcng  3818  sbcrext  3855  cbvrexcsf  3925  difjust  3937  eldif  3945  dfpss3  4062  dfdif3  4090  difeq2  4092  disjne  4402  pssdifcom1  4433  eldifpr  4589  elpwunsn  4615  eldiftp  4618  preqsnd  4783  disjxun  5056  nalset  5209  dtru  5263  dtruALT  5280  rexxfrd  5301  rexxfr2d  5303  rexxfrd2  5305  rexxfr  5308  dtruALT2  5327  opthneg  5365  snopeqop  5388  otiunsndisj  5402  poeq1  5471  pocl  5475  swopo  5478  sotric  5495  sotrieq  5496  isso2i  5502  somo  5504  freq1  5519  frirr  5526  fr2nr  5527  frminex  5529  tz7.2  5533  wereu2  5546  poinxp  5626  frinxp  5628  posn  5631  frsn  5633  rexiunxp  5705  rexxpf  5712  intirr  5972  poirr2  5978  cnvpo  6132  predpoirr  6170  predfrirr  6171  nordeq  6204  ordtri1  6218  ordtri3  6221  fvmpti  6761  fndmdif  6805  rexrnmptw  6854  rexrnmpt  6856  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  7482  dfwe2  7484  ordsucsssuc  7526  nlimsucg  7545  orduninsuc  7546  dfom2  7570  ssnlim  7587  f1oweALT  7664  frxp  7811  poxp  7813  suppofssd  7858  wfrlem10  7955  smoword  7994  tz7.48lem  8068  oacan  8164  oaword  8165  omlimcl  8194  omeulem1  8198  nnaword  8243  nnmword  8249  nneob  8269  brdifun  8308  swoer  8309  undifixp  8487  boxcutc  8494  2dom  8571  php  8690  nndomo  8701  nnsdomo  8702  unxpdomlem2  8712  frfi  8752  unfilem1  8771  supeq3  8902  supeq123d  8903  supmo  8905  eqsup  8909  supub  8912  sup0  8919  suppr  8924  supisolem  8926  supisoex  8927  eqinf  8937  infval  8939  infmo  8948  infpr  8956  infempty  8960  oieq1  8965  ordtypecbv  8970  ordtypelem7  8977  wemapsolem  9003  canthwdom  9032  zfregcl  9047  elirrv  9049  elirr  9050  noinfep  9112  cantnfp1lem3  9132  rankr1clem  9238  carden2b  9385  domtri2  9407  alephord3  9493  alephdom2  9502  alephval3  9525  dfac9  9551  kmlem2  9566  kmlem4  9568  isfin4  9708  isfin7  9712  fin23lem11  9728  isf32lem5  9768  isf34lem4  9788  fin1a2lem6  9816  fin1a2lem7  9817  fin1a2lem12  9822  itunisuc  9830  ac6n  9896  zorn2g  9914  zornn0g  9916  ttukeylem7  9926  axpowndlem3  10010  axpowndlem4  10011  axregnd  10015  elgch  10033  engch  10039  fpwwe2lem13  10053  fpwwe2  10054  pwfseqlem1  10069  pwfseqlem3  10071  hargch  10084  addnidpi  10312  pinq  10338  nqereu  10340  ltsonq  10380  prlem934  10444  ltexprlem7  10453  addcanpr  10457  prlem936  10458  reclem2pr  10459  reclem3pr  10460  supexpr  10465  ltsosr  10505  supsrlem  10522  axpre-lttri  10576  axpre-sup  10580  xrlenlt  10695  axlttri  10701  axsup  10705  ltne  10726  dedekind  10792  readdcan  10803  leadd1  11097  ltsub1  11125  ltsub2  11126  leord1  11156  lediv1  11494  lemuldiv  11509  lerec  11512  le2msq  11529  infm3  11589  suprnub  11595  infregelb  11614  avgle1  11866  avgle2  11867  znnnlt1  11998  indstr  12305  zsupss  12326  uzsupss  12329  rpneg  12411  xralrple  12588  xleneg  12601  xltadd1  12639  xposdif  12645  xmulneg1  12652  xltmul1  12675  xrsupexmnf  12688  xrinfmexpnf  12689  xrsupsslem  12690  xrinfmsslem  12691  xrub  12695  supxrleub  12709  infxrgelb  12718  difreicc  12860  nn0disj  13013  nelfzo  13033  elfznelfzo  13132  fvinim0ffz  13146  injresinjlem  13147  ssnn0fi  13343  leexp2  13525  hashbnd  13686  hasheni  13698  hashbc  13801  wrdsymb0  13891  swrdnd  14006  swrdnd2  14007  pfxnd0  14040  repswswrd  14136  repswccat  14138  cshwidxmod  14155  cnpart  14589  sqrtlt  14611  limsuplt  14826  rlimrege0  14926  isercoll  15014  efle  15461  odd2np1  15680  sumodd  15729  divalglem7  15740  ndvdsadd  15751  fldivndvdslt  15755  bitsfval  15762  bitsval  15763  bits0  15767  bitsp1  15770  bitsmod  15775  bitscmp  15777  bitsinv1lem  15780  sadadd2lem2  15789  saddisjlem  15803  bitsshft  15814  gcdneg  15860  algcvgblem  15911  lcmneg  15937  isprm3  16017  dvdsnprmd  16024  isprm5  16041  rpexp  16054  phiprmpw  16103  m1dvdsndvds  16125  pythagtrip  16161  pcgcd1  16203  prmpwdvds  16230  prmreclem2  16243  prmreclem3  16244  prmreclem5  16246  prmreclem6  16247  vdwlem6  16312  vdwnnlem2  16322  vdwnnlem3  16323  vdwnn  16324  prmlem0  16429  prmlem1a  16430  divsfval  16810  mrisval  16891  ismri  16892  ismri2dad  16898  cidpropd  16970  plttr  17570  joinval  17605  meetval  17619  acsfiindd  17777  isnsgrp  17895  mgm2nsgrplem2  18024  sgrp2nmndlem3  18030  symgfix2  18475  pmtrdifellem4  18538  psgnunilem1  18552  psgnunilem5  18553  psgnunilem2  18554  psgnunilem3  18555  pmtrsn  18578  sylow1lem3  18656  sylow2alem2  18674  efgsfo  18796  ablfac1eulem  19125  ablfac1eu  19126  pgpfac1lem1  19127  pgpfac1lem5  19132  islbs  19779  lbsind  19783  lbspss  19785  lbspropd  19802  lspsnne1  19820  islbs2  19857  lbsacsbs  19859  lbsextlem1  19861  lbsextlem3  19863  lbsextlem4  19864  lbsextg  19865  nzrunit  19970  opsrtoslem2  20195  cply1coe0  20397  cply1coe0bi  20398  frlmlbs  20871  islindf  20886  islinds2  20887  islindf2  20888  lindfind  20890  lindsind  20891  lindfrn  20895  lindfmm  20901  lsslindf  20904  islindf4  20912  mdetunilem7  21157  mdetunilem8  21158  mdetunilem9  21159  maducoeval2  21179  pmatcollpw3fi1lem1  21324  fvmptnn04ifa  21388  fvmptnn04ifc  21390  fvmptnn04ifd  21391  chfacffsupp  21394  chfacfscmul0  21396  chfacfpmmul0  21400  elcls  21611  maxlp  21685  perfi  21693  ordtbaslem  21726  ordtval  21727  ordtbas2  21729  ordtopn1  21732  ordtopn2  21733  ordtcnv  21739  ordtrest  21740  ordtrest2lem  21741  ordtrest2  21742  pnfnei  21758  mnfnei  21759  isreg2  21915  ordthauslem  21921  cmpfi  21946  cmpfii  21947  bwth  21948  nconnsubb  21961  hausdiag  22183  txkgen  22190  kqdisj  22270  ordthmeolem  22339  fbfinnfr  22379  trfbas  22382  fbunfip  22407  fbasrn  22422  trfil3  22426  ufileu  22457  fin1aufil  22470  hausflim  22519  alexsubALTlem2  22586  alexsubALTlem3  22587  alexsubALTlem4  22588  ptcmplem2  22591  ptcmplem3  22592  stdbdbl  23056  iccntr  23358  reconnlem2  23364  iccpnfcnv  23477  xrhmeo  23479  lebnumlem1  23494  lebnumlem2  23495  lebnumlem3  23496  bcthlem4  23859  minveclem3b  23960  ivthlem2  23982  ivthlem3  23983  mbfmax  24179  mbfposr  24182  i1fd  24211  mbfi1fseqlem4  24248  itg2splitlem  24278  itg2monolem1  24280  itg2cnlem1  24291  dvne0  24537  lhop1lem  24539  deg1nn0clb  24613  dgrle  24762  coemulhi  24773  aaliou3lem9  24868  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  25527  ftalem7  25584  isppw2  25620  musum  25696  dchrsum2  25772  bposlem1  25788  lgsmod  25827  lgsdir2lem2  25830  lgsdir2  25834  lgsne0  25839  lgsprme0  25843  gausslemma2dlem4  25873  lgsquadlem1  25884  2lgslem3  25908  2lgsoddprm  25920  2sq2  25937  addsqrexnreu  25946  rpvmasumlem  25991  padicabv  26134  ostth3  26142  ostth  26143  istrkgld  26173  axtgupdim2  26185  tglowdim2l  26364  axlowdimlem16  26671  axlowdim2  26674  axlowdim  26675  numedglnl  26857  usgredg2v  26937  lfuhgr1v0e  26964  cusgrfi  27168  vtxd0nedgb  27198  vtxduhgr0edgnel  27204  1loopgrnb0  27212  1hevtxdg0  27215  vtxdgoddnumeven  27263  wlkp1lem1  27383  wlkp1lem2  27384  wlkp1lem5  27387  crctcsh  27530  clwlkclwwlklem2a4  27703  eupth2eucrct  27924  eupth2lem3lem3  27937  eupth2lem3lem4  27938  eupth2lem3lem6  27940  eupth2lem3lem7  27941  eupth2lems  27945  eupth2  27946  konigsberglem4  27962  nfrgr2v  27979  frgrwopreglem3  28021  fusgr2wsp2nb  28041  frgrreggt1  28100  friendshipgt3  28105  lpni  28185  nmobndseqi  28484  minvecolem5  28586  chpsscon3  29208  chnle  29219  nonbooli  29356  pjnel  29431  specval  29603  nmcfnlbi  29757  stri  29962  hstri  29970  cvbr  29987  cvcon3  29989  chcv1  30060  cvexchlem  30073  chrelat2  30075  nelun  30202  elpreq  30218  nelpr  30219  ifeqeqx  30225  nfpconfp  30306  isoun  30364  suppss3  30387  xrge0infss  30411  infxrge0gelb  30417  eliccelico  30427  elicoelioo  30428  nndiffz1  30436  hashgt1  30457  nn0min  30464  toslublem  30582  tosglblem  30584  pmtrcnel  30661  cycpmco2  30703  isarchi2  30742  archiabl  30755  0nellinds  30863  lindssn  30867  lindfpropd  30870  lbslsat  30914  lindsunlem  30920  ordtcnvNEW  31063  ordtrestNEW  31064  ordtrest2NEWlem  31065  ordtrest2NEW  31066  ordtconnlem1  31067  xrge0iifcnv  31076  esumpcvgval  31237  esum2d  31252  ddemeas  31395  omssubadd  31458  oddpwdc  31512  eulerpartlems  31518  eulerpartlemf  31528  eulerpartlemt  31529  eulerpartlemr  31532  eulerpartlemgvv  31534  eulerpartlemn  31539  ballotlemfc0  31650  ballotlemfcc  31651  ballotlem4  31656  ballotlemimin  31663  ballotlem7  31693  plymulx  31718  signsply0  31721  reprinfz1  31793  reprpmtf1o  31797  reprdifc  31798  hgt750lema  31828  hgt750leme  31829  istrkg2d  31837  bnj23  31888  bnj1185  31965  bnj1228  32181  bnj1388  32203  bnj1417  32211  hashfundm  32252  revwlk  32269  isacycgr  32290  acycgr0v  32293  prclisacycgr  32296  erdszelem10  32345  satf0n0  32523  fmlaomn0  32535  fmlasucdisj  32544  satfv1fvfmla1  32568  satefvfmla1  32570  ismfs  32694  mvtinf  32700  untelirr  32832  untsucf  32834  untangtr  32838  ceqsralv2  32854  dfpo2  32889  dfon2lem3  32928  dfon2lem4  32929  dfon2lem7  32932  dfon2lem9  32934  distel  32946  frpomin  32976  soseq  32994  noextenddif  33073  nodenselem4  33089  nodenselem5  33090  nodenselem7  33092  nolt02o  33097  noresle  33098  noprefixmo  33100  nosupdm  33102  nosupfv  33104  nosupres  33105  nosupbnd1lem1  33106  nosupbnd1lem3  33108  nosupbnd1lem5  33110  nosupbnd1  33112  nosupbnd2lem1  33113  nosupbnd2  33114  slenlt  33129  nocvxminlem  33145  slerec  33175  funpartfv  33304  dfrdg4  33310  nn0prpwlem  33568  nn0prpw  33569  limsucncmpi  33691  limsucncmp  33692  ordcmp  33693  unblimceq0  33744  unbdqndv1  33745  bj-hbntbi  33936  bj-cbvexdv  34020  bj-dtru  34037  bj-ru0  34151  bj-nuliota  34245  topdifinffinlem  34511  topdifinffin  34512  icorempo  34515  relowlpssretop  34528  finxpreclem2  34554  finxpreclem6  34560  wl-ax11-lem8  34706  wl-dfrexf  34729  leceifl  34763  lindsadd  34767  lindsenlbs  34769  matunitlindflem1  34770  poimirlem16  34790  poimirlem17  34791  poimirlem18  34792  poimirlem19  34793  poimirlem21  34795  poimirlem23  34797  poimirlem26  34800  poimirlem27  34801  poimirlem28  34802  poimirlem31  34805  poimir  34807  mblfinlem2  34812  mblfinlem3  34813  ismblfin  34815  cnambfre  34822  itg2addnclem  34825  itg2addnclem2  34826  iblabsnclem  34837  ftc1anclem1  34849  areacirc  34869  heibor1lem  34970  heiborlem1  34972  heiborlem6  34977  heiborlem8  34979  heiborlem10  34981  smprngopr  35213  ecin0  35489  ax12inda  35966  riotaclbgBAD  35972  lcvfbr  36038  lcvbr  36039  lsatcv0  36049  l1cvpat  36072  opltcon3b  36222  cvrfval  36286  cvrval  36287  cvrnbtwn  36289  cvrval2  36292  cvrnbtwn2  36293  cvrnbtwn3  36294  cvrcon3b  36295  cvrnbtwn4  36297  atnlt  36331  iscvlat  36341  cvlexch1  36346  hlsuprexch  36399  hlrelat5N  36419  hlrelat2  36421  cvrval5  36433  3dimlem1  36476  3dim1lem5  36484  3dim2  36486  3dim3  36487  llnnlt  36541  islpln5  36553  lplni2  36555  lvolex3N  36556  lplnnle2at  36559  islpln2a  36566  lplnribN  36569  lplnexllnN  36582  lplnnlt  36583  lvoli3  36595  islvol5  36597  lvoli2  36599  lvolnle3at  36600  islvol2aN  36610  4atlem11  36627  lvolnltN  36636  dalawlem15  36903  4atexlemex2  37089  4atex  37094  4atex2-0aOLDN  37096  4atex2-0cOLDN  37098  lautcvr  37110  ltrnfset  37135  ltrnset  37136  ltrnu  37139  trlfset  37178  trlset  37179  trlval2  37181  cdlemd6  37221  cdleme0nex  37308  cdleme18d  37313  cdleme25b  37372  cdleme25cv  37376  cdleme29b  37393  cdleme31fv  37408  cdleme31fv2  37411  cdlemefrs29bpre0  37414  cdlemefr32sn2aw  37422  cdlemefr29bpre0N  37424  cdlemefr29clN  37425  cdlemefr32fvaN  37427  cdlemefr32fva1  37428  cdlemefs32sn1aw  37432  cdleme32fva  37455  cdleme32fvaw  37457  cdleme40v  37487  cdleme42b  37496  cdleme46f2g2  37511  cdleme46f2g1  37512  cdleme48gfv  37555  cdlemg1fvawlemN  37591  cdlemg1cex  37606  cdlemg6d  37639  cdlemm10N  38136  dicffval  38192  dicfval  38193  dicval  38194  dicfnN  38201  dicvalrelN  38203  dihffval  38248  dihfval  38249  dihlsscpre  38252  dvh4dimat  38456  dvh3dimatN  38457  dvh4dimlem  38461  dvh3dim  38464  dvh4dimN  38465  dvh3dim2  38466  dvh3dim3N  38467  mapdcv  38678  mapdh9aOLDN  38808  hdmapfval  38845  hdmapval  38846  hdmapval2  38850  hdmap11lem2  38860  oexpreposd  39059  ellz1  39244  rencldnfilem  39297  jm2.22  39472  jm2.23  39473  wepwsolem  39522  fnwe2lem2  39531  aomclem8  39541  unxpwdom3  39575  ifpbi12  39734  dfsucon  39769  nndomog  39777  ss2iundf  39884  frege124d  39986  clsk3nimkb  40270  clsk1indlem1  40275  clsk1independent  40276  ntrneineine1lem  40314  ntrneicls11  40320  clsneiel1  40338  clsneiel2  40339  neicvgel1  40349  neicvgel2  40350  radcnvrat  40526  rusbcALT  40651  en3lpVD  41059  eliin2f  41251  nssd  41252  wessf1ornlem  41325  limsupre2lem  41885  icccncfext  42050  stoweidlem14  42180  stoweidlem34  42200  stoweidlem59  42225  etransclem24  42424  nnfoctbdjlem  42618  nnfoctbdj  42619  hspmbllem2  42790  smfmbfcex  42917  nsssmfmbflem  42935  eu2ndop1stv  43205  afvfv0bi  43232  afvco2  43256  ndmaovg  43264  ndfatafv2nrn  43301  afv2ndefb  43304  afv2fv0  43345  nelbr  43354  otiunsndisjX  43359  fun2dmnopgexmpl  43364  ltnltne  43380  readdcnnred  43384  resubcnnred  43385  recnmulnred  43386  cndivrenred  43387  ichnreuop  43481  fmtnoinf  43545  odz2prm2pw  43572  prmdvdsfmtnof1lem2  43594  lighneallem3  43619  lighneallem4  43622  requad1  43634  isodd3  43664  bits0ALTV  43691  nfermltl8rev  43754  nfermltl2rev  43755  nfermltlrev  43756  smndex1n0mnd  43982  lidldomnnring  44099  zrninitoringc  44240  ztprmneprm  44293  lindepsnlininds  44405  islindeps  44406  lindslinindsimp2lem5  44415  lindslinindsimp2  44416  difmodm1lt  44480  line2ylem  44636  line2xlem  44638  elsetrecslem  44699
  Copyright terms: Public domain W3C validator