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

Theorem notbid 303
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 299 . . 3 (𝜓 ↔ ¬ ¬ 𝜓)
3 notnotb 299 . . 3 (𝜒 ↔ ¬ ¬ 𝜒)
41, 2, 33bitr3g 297 . 2 (𝜑 → (¬ ¬ 𝜓 ↔ ¬ ¬ 𝜒))
54con4bid 302 1 (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 191
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 192
This theorem is referenced by:  notbi  304  ifpbi123d  1011  con3ALT  1016  con3OLD  1019  nanbi1  1437  xorbi12d  1463  cbvexvw  1918  hba1w  1922  hbe1w  1923  cbvexv1  2117  cbvex  2162  cbvexd  2166  cbvex2  2168  drex1  2210  eujustALT  2356  necon3abid  2713  neleq12d  2782  cbvrexf  3035  gencbval  3115  spcegf  3151  spc2gv  3158  spc3gv  3160  cdeqnot  3279  ru  3290  sbcng  3332  sbcrext  3365  cbvrexcsf  3418  difjust  3428  eldif  3436  dfpss3  3541  difeq2  3570  disjne  3850  pssdifcom1  3880  pssdifcom2  3881  eldifpr  4021  elpwunsn  4040  eldiftp  4043  prel12  4181  prel12g  4185  disjxun  4432  nalset  4573  pwnss  4606  dtru  4633  rexxfrd  4654  rexxfr2d  4656  rexxfrd2  4658  rexxfr  4661  dtruALT  4673  dtruALT2  4685  opthneg  4722  otiunsndisj  4748  poeq1  4804  pocl  4808  swopo  4811  sotric  4827  sotrieq  4828  isso2i  4833  somo  4835  freq1  4850  frirr  4857  fr2nr  4858  frminex  4860  tz7.2  4864  wereu2  4877  poinxp  4945  frinxp  4947  posn  4950  frsn  4952  rexiunxp  5022  rexxpf  5029  intirr  5268  poirr2  5274  cnvpo  5425  predpoirr  5459  predfrirr  5460  nordeq  5493  ordtri1  5507  ordtri3  5510  fvmpti  6014  fndmdif  6053  rexrnmpt  6099  f1imapss  6238  cbvexfo  6259  soisoi  6292  isopolem  6309  weniso  6318  canth  6322  riotaclb  6362  rexrnmpt2  6487  ndmovg  6527  sorpssuni  6656  sorpssint  6657  fr3nr  6683  dfwe2  6685  ordsucsssuc  6727  nlimsucg  6746  orduninsuc  6747  dfom2  6771  ssnlim  6787  f1oweALT  6854  frxp  6985  poxp  6987  wfrlem10  7122  smoword  7162  tz7.48lem  7235  oacan  7326  oaword  7327  omlimcl  7356  omeulem1  7360  nnaword  7405  nnmword  7411  nneob  7430  brdifun  7469  swoer  7470  undifixp  7641  boxcutc  7648  2dom  7726  php  7840  nndomo  7850  nnsdomo  7851  unxpdomlem2  7861  frfi  7901  unfilem1  7920  supeq3  8048  supeq123d  8049  supmo  8051  eqsup  8055  supub  8058  sup0  8065  suppr  8070  supisolem  8072  supisoex  8073  eqinf  8083  infval  8085  infmo  8094  infpr  8102  infempty  8105  oieq1  8110  ordtypecbv  8115  ordtypelem7  8122  wemapsolem  8148  canthwdom  8177  zfregcl  8192  zfregclOLD  8194  elirrv  8197  elirr  8198  noinfep  8250  cantnfp1lem3  8270  rankr1clem  8376  carden2b  8486  domtri2  8508  alephord3  8594  alephdom2  8603  alephval3  8626  dfac9  8651  kmlem2  8666  kmlem4  8668  isfin4  8812  isfin7  8816  fin23lem11  8832  isf32lem5  8872  isf34lem4  8892  fin1a2lem6  8920  fin1a2lem7  8921  fin1a2lem12  8926  itunisuc  8934  ac6n  9000  zorn2g  9018  zornn0g  9020  ttukeylem7  9030  axpowndlem3  9109  axpowndlem4  9110  axregnd  9114  elgch  9132  engch  9138  fpwwe2lem13  9152  fpwwe2  9153  pwfseqlem1  9168  pwfseqlem3  9170  hargch  9183  addnidpi  9411  pinq  9437  nqereu  9439  ltsonq  9479  prlem934  9543  ltexprlem7  9552  addcanpr  9556  prlem936  9557  reclem2pr  9558  reclem3pr  9559  supexpr  9564  ltsosr  9603  supsrlem  9620  axpre-lttri  9674  axpre-sup  9678  xrlenlt  9784  axlttri  9790  axsup  9794  ltne  9815  dedekind  9882  readdcan  9892  leadd1  10170  ltsub1  10198  ltsub2  10199  leord1  10229  lediv1  10559  lemuldiv  10575  lerec  10578  le2msq  10595  lbinf  10648  lbinfmOLD  10649  infm3  10657  suprnub  10661  infregelb  10683  infmrgelbOLD  10684  infmrlbOLD  10686  avgle1  10942  avgle2  10943  znnnlt1  11055  indstr  11317  zsupss  11344  uzsupss  11347  rpneg  11423  xralrple  11591  xleneg  11604  xltadd1  11637  xposdif  11643  xmulneg1  11650  xltmul1  11673  xrsupexmnf  11685  xrinfmexpnf  11686  xrsupsslem  11687  xrinfmsslem  11688  xrub  11692  supxrleub  11707  infxrgelb  11716  infmxrgelbOLD  11720  difreicc  11860  nn0disj  12006  nelfzo  12026  elfznelfzo  12120  fvinim0ffz  12130  injresinjlem  12131  ssnn0fi  12311  leexp2  12441  hashbnd  12635  hasheni  12645  hashbc  12739  wrdsymb0  12833  swrdnd  12922  swrdnd2  12923  repswswrd  13020  repswccat  13021  cshwidxmod  13038  cnpart  13463  sqrtlt  13485  limsuplt  13698  limsupltOLD  13699  rlimrege0  13803  isercoll  13891  efle  14332  odd2np1  14526  divalglem7  14541  ndvdsadd  14551  bitsfval  14558  bitsval  14559  bits0  14563  bitsp1  14566  bitsmod  14572  bitscmp  14574  bitsinv1lem  14577  sadadd2lem2  14586  saddisjlem  14600  bitsshft  14611  gcdneg  14652  algcvgblem  14698  lcmneg  14730  isprm3  14795  isprm5  14813  rpexp  14834  phiprmpw  14886  m1dvdsndvds  14911  pythagtrip  14946  pcgcd1  14988  prmpwdvds  15010  prmreclem2  15023  prmreclem3  15024  prmreclem5  15026  prmreclem6  15027  vdwlem6  15098  vdwnnlem2  15108  vdwnnlem3  15109  vdwnn  15110  prmo1  15157  prmlem0  15238  prmlem1a  15239  divsfval  15618  mrisval  15701  ismri  15702  ismri2dad  15708  cidpropd  15781  plttr  16381  joinval  16416  meetval  16430  acsfiindd  16588  isnsgrp  16696  mgm2nsgrplem2  16813  sgrp2nmndlem3  16819  symgfix2  17218  pmtrdifellem4  17281  psgnunilem1  17295  psgnunilem5  17296  psgnunilem2  17297  psgnunilem3  17298  pmtrsn  17321  sylow1lem3  17413  sylow2alem2  17431  efgsfo  17550  ablfac1eulem  17865  ablfac1eu  17866  pgpfac1lem1  17867  pgpfac1lem5  17872  islbs  18459  lbsind  18463  lbspss  18465  lbspropd  18482  lspsnne1  18500  islbs2  18537  lbsacsbs  18539  lbsextlem1  18541  lbsextlem3  18543  lbsextlem4  18544  lbsextg  18545  nzrunit  18650  opsrtoslem2  18867  cply1coe0  19051  cply1coe0bi  19052  frlmlbs  19513  islindf  19528  islinds2  19529  islindf2  19530  lindfind  19532  lindsind  19533  lindfrn  19537  lindfmm  19543  lsslindf  19546  islindf4  19554  mdetunilem7  19801  mdetunilem8  19802  mdetunilem9  19803  maducoeval2  19823  pmatcollpw3fi1lem1  19968  fvmptnn04ifa  20032  fvmptnn04ifc  20034  fvmptnn04ifd  20035  chfacffsupp  20038  chfacfscmul0  20040  chfacfpmmul0  20044  elcls  20246  maxlp  20320  perfi  20328  ordtbaslem  20361  ordtval  20362  ordtbas2  20364  ordtopn1  20367  ordtopn2  20368  ordtcnv  20374  ordtrest  20375  ordtrest2lem  20376  ordtrest2  20377  pnfnei  20393  mnfnei  20394  isreg2  20550  ordthauslem  20556  cmpfi  20580  cmpfii  20581  bwth  20582  nconsubb  20595  hausdiag  20817  txkgen  20824  kqdisj  20904  ordthmeolem  20973  fbfinnfr  21014  trfbas  21017  fbunfip  21042  fbasrn  21057  trfil3  21061  ufileu  21092  fin1aufil  21105  hausflim  21154  alexsubALTlem2  21221  alexsubALTlem3  21222  alexsubALTlem4  21223  ptcmplem2  21226  ptcmplem3  21227  stdbdbl  21690  iccntr  21997  reconnlem2  22003  iccpnfcnv  22130  xrhmeo  22132  lebnumlem1  22147  lebnumlem2  22148  lebnumlem3  22149  lebnumlem1OLD  22150  lebnumlem2OLD  22151  lebnumlem3OLD  22152  bcthlem4  22454  minveclem3b  22529  minveclem3bOLD  22541  ivthlem2  22562  ivthlem3  22563  mbfmax  22766  mbfposr  22769  i1fd  22800  mbfi1fseqlem4  22837  itg2splitlem  22867  itg2monolem1  22869  itg2cnlem1  22880  dvne0  23124  lhop1lem  23126  deg1nn0clb  23200  dgrle  23358  coemulhi  23369  aaliou3lem9  23467  cos11  23643  logleb  23713  argrege0  23721  logdivle  23732  ellogdm  23745  cxple  23801  cxplt2  23804  cxple3  23807  isosctrlem1  23908  atandm  23963  atans2  24018  atantayl2  24025  eldmgm  24108  ftalem7  24166  isppw2  24203  musum  24281  dchrsum2  24357  bposlem1  24373  lgsmod  24410  lgsdir2lem2  24413  lgsdir2  24417  lgsne0  24422  lgsquadlem1  24443  rpvmasumlem  24486  padicabv  24629  ostth3  24637  ostth  24638  istrkgld  24668  axtgupdim2  24680  tglowdim2l  24856  axlowdimlem16  25148  axlowdim2  25151  axlowdim  25152  usgra1v  25278  usgraidx2v  25281  nbgra0nb  25318  cusgrafilem3  25370  spthispth  25464  wlkdvspthlem  25498  clwlkisclwwlklem2a4  25673  clwlknclwlkdifs  25848  eupath2lem3  25867  eupath2  25868  konigsberg  25875  frgra2v  25887  frgrancvvdeqlem2  25919  2spotiundisj  25950  usg2spot2nb  25953  2spotmdisj  25956  frgrareggt1  26004  friendshipgt3  26009  lpni  26072  nmobndseqi  26583  minvecolem5  26686  minvecolem5OLD  26696  chpsscon3  27319  chnle  27330  nonbooli  27467  pjnel  27542  specval  27714  nmcfnlbi  27868  stri  28073  hstri  28081  cvbr  28098  cvcon3  28100  chcv1  28171  cvexchlem  28184  chrelat2  28186  spc2d  28270  elpreq  28317  ifeqeqx  28318  ifbieq12d2  28319  isoun  28439  suppss3  28468  xrge0infss  28496  xrge0infssOLD  28497  xrge0infssdOLD  28499  infxrge0lbOLD  28503  infxrge0gelb  28506  infxrge0gelbOLD  28507  eliccelico  28515  elicoelioo  28516  nndiffz1  28522  nn0min  28540  toslublem  28584  tosglblem  28586  isarchi2  28657  archiabl  28670  ordtcnvNEW  28881  ordtrestNEW  28882  ordtrest2NEWlem  28883  ordtrest2NEW  28884  ordtconlem1  28885  xrge0iifcnv  28894  elzdif0  28939  esumpcvgval  29054  esum2d  29069  ddemeas  29213  omssubadd  29282  oms0OLD  29283  omssubaddOLD  29286  oddpwdc  29341  eulerpartlems  29347  eulerpartlemf  29357  eulerpartlemt  29358  eulerpartlemr  29361  eulerpartlemgvv  29363  eulerpartlemn  29368  ballotlemfc0  29479  ballotlemfcc  29480  ballotlem4  29485  ballotlemimin  29492  ballotlem7  29522  ballotlemiminOLD  29530  ballotlem7OLD  29560  plymulx  29590  signsply0  29593  istrkg2d  29636  bnj23  29677  bnj1185  29757  bnj1476  29810  bnj1228  29972  bnj1388  29994  bnj1417  30002  erdszelem10  30075  ismfs  30339  mvtinf  30345  untelirr  30487  untsucf  30489  untangtr  30493  ceqsralv2  30510  inffz  30515  dfpo2  30546  dfon2lem3  30582  dfon2lem4  30583  dfon2lem7  30586  dfon2lem9  30588  distel  30601  soseq  30643  nodenselem4  30724  nodenselem5  30725  nocvxminlem  30730  nofulllem4  30745  funpartfv  30863  dfrdg4  30869  nn0prpwlem  31127  nn0prpw  31128  limsucncmpi  31254  limsucncmp  31255  ordcmp  31256  unblimceq0  31305  unbdqndv1  31306  bj-hbntbi  31483  bj-cbvexdv  31524  bj-cbvex2v  31526  bj-drex1v  31540  bj-nalset  31591  bj-dtru  31594  bj-ru0  31723  bj-nuliota  31809  topdifinffinlem  31971  topdifinffin  31972  icorempt2  31975  relowlpssretop  31988  finxpreclem2  32003  finxpreclem6  32009  wl-ax11-lem8  32147  leceifl  32167  lindsenlbs  32173  matunitlindflem1  32174  poimirlem16  32194  poimirlem17  32195  poimirlem18  32196  poimirlem19  32197  poimirlem21  32199  poimirlem23  32201  poimirlem26  32204  poimirlem27  32205  poimirlem28  32206  poimirlem31  32209  poimir  32211  mblfinlem2  32216  mblfinlem3  32217  ismblfin  32219  cnambfre  32227  dvtanlemOLD  32229  itg2addnclem  32231  itg2addnclem2  32232  iblabsnclem  32243  ftc1anclem1  32255  areacirc  32275  heibor1lem  32378  heiborlem1  32380  heiborlem6  32385  heiborlem8  32387  heiborlem10  32389  smprngopr  32522  ax12inda  32752  riotaclbgBAD  32759  lcvfbr  32826  lcvbr  32827  lsatcv0  32837  l1cvpat  32860  opltcon3b  33010  cvrfval  33074  cvrval  33075  cvrnbtwn  33077  cvrval2  33080  cvrnbtwn2  33081  cvrnbtwn3  33082  cvrcon3b  33083  cvrnbtwn4  33085  atnlt  33119  iscvlat  33129  cvlexch1  33134  hlsuprexch  33186  hlrelat5N  33206  hlrelat2  33208  cvrval5  33220  3dimlem1  33263  3dim1lem5  33271  3dim2  33273  3dim3  33274  llnnlt  33328  islpln5  33340  lplni2  33342  lvolex3N  33343  lplnnle2at  33346  islpln2a  33353  lplnribN  33356  lplnexllnN  33369  lplnnlt  33370  lvoli3  33382  islvol5  33384  lvoli2  33386  lvolnle3at  33387  islvol2aN  33397  4atlem11  33414  lvolnltN  33423  dalawlem15  33690  4atexlemex2  33876  4atex  33881  4atex2-0aOLDN  33883  4atex2-0cOLDN  33885  lautcvr  33897  ltrnfset  33922  ltrnset  33923  ltrnu  33926  trlfset  33966  trlset  33967  trlval2  33969  cdlemd6  34009  cdleme0nex  34096  cdleme18d  34101  cdleme25b  34161  cdleme25cv  34165  cdleme29b  34182  cdleme31fv  34197  cdleme31fv2  34200  cdlemefrs29bpre0  34203  cdlemefr32sn2aw  34211  cdlemefr29bpre0N  34213  cdlemefr29clN  34214  cdlemefr32fvaN  34216  cdlemefr32fva1  34217  cdlemefs32sn1aw  34221  cdleme32fva  34244  cdleme32fvaw  34246  cdleme40v  34276  cdleme42b  34285  cdleme46f2g2  34300  cdleme46f2g1  34301  cdleme48gfv  34344  cdlemg1fvawlemN  34380  cdlemg1cex  34395  cdlemg6d  34428  cdlemm10N  34926  dicffval  34982  dicfval  34983  dicval  34984  dicfnN  34991  dicvalrelN  34993  dihffval  35038  dihfval  35039  dihlsscpre  35042  dvh4dimat  35246  dvh3dimatN  35247  dvh4dimlem  35251  dvh3dim  35254  dvh4dimN  35255  dvh3dim2  35256  dvh3dim3N  35257  mapdcv  35468  mapdh9aOLDN  35599  hdmapfval  35638  hdmapval  35639  hdmapval2  35643  hdmap11lem2  35653  ellz1  35849  rencldnfilem  35903  jm2.22  36090  jm2.23  36091  wepwsolem  36140  fnwe2lem2  36149  aomclem8  36159  unxpwdom3  36193  ifpbi12  36372  ifpbi123  36374  relintabex  36426  ss2iundf  36490  frege124d  36592  ntrneineine1lem  36897  ntrneicls11  36901  clsneiel1  36910  clsneiel2  36911  neicvgel1  36916  neicvgel2  36917  radcnvrat  37020  rusbcALT  37147  en3lpVD  37589  wessf1ornlem  37819  icccncfext  38174  stoweidlem14  38310  stoweidlem34  38331  stoweidlem59  38356  etransclem24  38559  nnfoctbdjlem  38743  nnfoctbdj  38744  hspmbllem2  38912  eu2ndop1stv  39143  afvfv0bi  39174  afvco2  39198  ndmaovg  39206  isodd3  39302  bits0ALTV  39328  otiunsndisjX  39527  2f1fvneq  39533  fun2dmnopgexmpl  39551  ltnltne  39568  usgredg2v  39854  lfuhgr1v0e  39880  cusgrfi  40074  vtxd0nedgb  40103  vtxduhgr0edgnel  40109  1loopgrnb0  40117  1hevtxdg0  40120  1wlkp1lem1  40282  1wlkp1lem2  40283  1wlkp1lem5  40286  crctcsh  40427  clwwlknclwwlkdifs  40581  clwlkclwwlklem2a4  40606  eupth2eucrct  40785  eupth2lem3lem3  40798  eupth2lem3lem4  40799  eupth2lem3lem6  40801  eupth2lem3lem7  40802  eupth2lems  40806  eupth2  40807  konigsberglem4  40825  nfrgr2v  40842  frgrncvvdeqlem2  40870  fusgr2wsp2nb  40898  av-frgrareggt1  40947  av-friendshipgt3  40952  lidldomnnring  41120  zrninitoringc  41263  ztprmneprm  41318  lindepsnlininds  41435  islindeps  41436  lindslinindsimp2lem5  41445  lindslinindsimp2  41446  difmodm1lt  41514
  Copyright terms: Public domain W3C validator