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

Theorem notbid 321
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 318 . . 3 (𝜓 ↔ ¬ ¬ 𝜓)
3 notnotb 318 . . 3 (𝜒 ↔ ¬ ¬ 𝜒)
41, 2, 33bitr3g 316 . 2 (𝜑 → (¬ ¬ 𝜓 ↔ ¬ ¬ 𝜒))
54con4bid 320 1 (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209
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 210
This theorem is referenced by:  notbi  322  annotanannot  833  ifpbi123dOLD  1076  con3ALT  1082  xorbi12d  1518  norassOLD  1535  equsexvw  2012  cbvexvw  2045  cbvexdvaw  2047  hbe1w  2056  cbvexv1  2364  cbvex2v  2367  drex1v  2390  cbvex  2419  cbvexvOLD  2423  cbvex2  2436  drex1  2465  eujustALT  2658  necon3abid  3050  neleq12d  3122  cbvrexfw  3423  cbvrexf  3425  cbvrexdva2OLD  3444  gencbval  3537  spcegf  3577  spc2gv  3587  spc2d  3589  spc3gv  3591  cdeqnot  3745  rru  3756  ru  3757  sbcng  3804  sbcrext  3840  cbvrexcsf  3909  difjust  3921  eldif  3929  dfpss3  4049  dfdif3  4077  difeq2  4079  disjne  4387  pssdifcom1  4418  eldifpr  4582  elpwunsn  4606  eldiftp  4609  preqsnd  4774  disjxun  5051  nalset  5204  dtru  5259  dtruALT  5277  rexxfrd  5298  rexxfr2d  5300  rexxfrd2  5302  rexxfr  5305  dtruALT2  5324  opthneg  5361  snopeqop  5384  otiunsndisj  5398  poeq1  5465  pocl  5469  swopo  5472  sotric  5489  sotrieq  5490  isso2i  5496  somo  5498  freq1  5513  frirr  5520  fr2nr  5521  frminex  5523  tz7.2  5527  wereu2  5540  poinxp  5620  frinxp  5622  posn  5625  frsn  5627  rexiunxp  5699  rexxpf  5706  intirr  5966  poirr2  5972  cnvpo  6126  predpoirr  6164  predfrirr  6165  nordeq  6198  ordtri1  6212  ordtri3  6215  fvmpti  6756  fndmdif  6801  rexrnmptw  6850  rexrnmpt  6852  2f1fvneq  7008  f1imapss  7014  cbvexfo  7036  nf1const  7049  soisoi  7071  isopolem  7088  weniso  7097  canth  7101  riotaclb  7145  rexrnmpo  7280  ndmovg  7322  sorpssuni  7449  sorpssint  7450  fr3nr  7485  dfwe2  7487  ordsucsssuc  7529  nlimsucg  7548  orduninsuc  7549  dfom2  7573  ssnlim  7590  f1oweALT  7665  frxp  7812  poxp  7814  suppofssd  7859  wfrlem10  7956  smoword  7995  tz7.48lem  8069  oacan  8166  oaword  8167  omlimcl  8196  omeulem1  8200  nnaword  8245  nnmword  8251  nneob  8271  brdifun  8310  swoer  8311  undifixp  8490  boxcutc  8497  2dom  8574  php  8694  nndomog  8701  nnsdomo  8707  unxpdomlem2  8716  frfi  8756  unfilem1  8775  supeq3  8906  supeq123d  8907  supmo  8909  eqsup  8913  supub  8916  sup0  8923  suppr  8928  supisolem  8930  supisoex  8931  eqinf  8941  infval  8943  infmo  8952  infpr  8960  infempty  8964  oieq1  8969  ordtypecbv  8974  ordtypelem7  8981  wemapsolem  9007  canthwdom  9036  zfregcl  9051  elirrv  9053  elirr  9054  noinfep  9116  cantnfp1lem3  9136  rankr1clem  9242  carden2b  9389  domtri2  9411  alephord3  9498  alephdom2  9507  alephval3  9530  dfac9  9556  kmlem2  9571  kmlem4  9573  isfin4  9713  isfin7  9717  fin23lem11  9733  isf32lem5  9773  isf34lem4  9793  fin1a2lem6  9821  fin1a2lem7  9822  fin1a2lem12  9827  itunisuc  9835  ac6n  9901  zorn2g  9919  zornn0g  9921  ttukeylem7  9931  axpowndlem3  10015  axpowndlem4  10016  axregnd  10020  elgch  10038  engch  10044  fpwwe2lem13  10058  fpwwe2  10059  pwfseqlem1  10074  pwfseqlem3  10076  hargch  10089  addnidpi  10317  pinq  10343  nqereu  10345  ltsonq  10385  prlem934  10449  ltexprlem7  10458  addcanpr  10462  prlem936  10463  reclem2pr  10464  reclem3pr  10465  supexpr  10470  ltsosr  10510  supsrlem  10527  axpre-lttri  10581  axpre-sup  10585  xrlenlt  10700  axlttri  10706  axsup  10710  ltne  10731  dedekind  10797  readdcan  10808  leadd1  11102  ltsub1  11130  ltsub2  11131  leord1  11161  lediv1  11499  lemuldiv  11514  lerec  11517  le2msq  11534  infm3  11594  suprnub  11600  infregelb  11619  avgle1  11872  avgle2  11873  znnnlt1  12004  indstr  12311  zsupss  12332  uzsupss  12335  rpneg  12416  xralrple  12593  xleneg  12606  xltadd1  12644  xposdif  12650  xmulneg1  12657  xltmul1  12680  xrsupexmnf  12693  xrinfmexpnf  12694  xrsupsslem  12695  xrinfmsslem  12696  xrub  12700  supxrleub  12714  infxrgelb  12723  difreicc  12869  nn0disj  13025  nelfzo  13045  elfznelfzo  13144  fvinim0ffz  13158  injresinjlem  13159  ssnn0fi  13355  leexp2  13538  hashbnd  13699  hasheni  13711  hashbc  13814  wrdsymb0  13899  swrdnd  14014  swrdnd2  14015  pfxnd0  14048  repswswrd  14144  repswccat  14146  cshwidxmod  14163  cnpart  14597  sqrtlt  14619  limsuplt  14834  rlimrege0  14934  isercoll  15022  efle  15469  odd2np1  15688  sumodd  15735  divalglem7  15746  ndvdsadd  15757  fldivndvdslt  15761  bitsfval  15768  bitsval  15769  bits0  15773  bitsp1  15776  bitsmod  15781  bitscmp  15783  bitsinv1lem  15786  sadadd2lem2  15795  saddisjlem  15809  bitsshft  15820  gcdneg  15866  algcvgblem  15917  lcmneg  15943  isprm3  16023  dvdsnprmd  16030  isprm5  16047  rpexp  16060  phiprmpw  16109  m1dvdsndvds  16131  pythagtrip  16167  pcgcd1  16209  prmpwdvds  16236  prmreclem2  16249  prmreclem3  16250  prmreclem5  16252  prmreclem6  16253  vdwlem6  16318  vdwnnlem2  16328  vdwnnlem3  16329  vdwnn  16330  prmlem0  16437  prmlem1a  16438  divsfval  16818  mrisval  16899  ismri  16900  ismri2dad  16906  cidpropd  16978  plttr  17578  joinval  17613  meetval  17627  acsfiindd  17785  isnsgrp  17903  smndex1n0mnd  18075  mgm2nsgrplem2  18082  sgrp2nmndlem3  18088  symgpssefmnd  18522  symgfix2  18542  pmtrdifellem4  18605  psgnunilem1  18619  psgnunilem5  18620  psgnunilem2  18621  psgnunilem3  18622  pmtrsn  18645  sylow1lem3  18723  sylow2alem2  18741  efgsfo  18863  ablfac1eulem  19192  ablfac1eu  19193  pgpfac1lem1  19194  pgpfac1lem5  19199  islbs  19843  lbsind  19847  lbspss  19849  lbspropd  19866  lspsnne1  19884  islbs2  19921  lbsacsbs  19923  lbsextlem1  19925  lbsextlem3  19927  lbsextlem4  19928  lbsextg  19929  nzrunit  20035  opsrtoslem2  20260  cply1coe0  20462  cply1coe0bi  20463  frlmlbs  20936  islindf  20951  islinds2  20952  islindf2  20953  lindfind  20955  lindsind  20956  lindfrn  20960  lindfmm  20966  lsslindf  20969  islindf4  20977  mdetunilem7  21222  mdetunilem8  21223  mdetunilem9  21224  maducoeval2  21244  pmatcollpw3fi1lem1  21389  fvmptnn04ifa  21453  fvmptnn04ifc  21455  fvmptnn04ifd  21456  chfacffsupp  21459  chfacfscmul0  21461  chfacfpmmul0  21465  elcls  21676  maxlp  21750  perfi  21758  ordtbaslem  21791  ordtval  21792  ordtbas2  21794  ordtopn1  21797  ordtopn2  21798  ordtcnv  21804  ordtrest  21805  ordtrest2lem  21806  ordtrest2  21807  pnfnei  21823  mnfnei  21824  isreg2  21980  ordthauslem  21986  cmpfi  22011  cmpfii  22012  bwth  22013  nconnsubb  22026  hausdiag  22248  txkgen  22255  kqdisj  22335  ordthmeolem  22404  fbfinnfr  22444  trfbas  22447  fbunfip  22472  fbasrn  22487  trfil3  22491  ufileu  22522  fin1aufil  22535  hausflim  22584  alexsubALTlem2  22651  alexsubALTlem3  22652  alexsubALTlem4  22653  ptcmplem2  22656  ptcmplem3  22657  stdbdbl  23122  iccntr  23424  reconnlem2  23430  iccpnfcnv  23547  xrhmeo  23549  lebnumlem1  23564  lebnumlem2  23565  lebnumlem3  23566  bcthlem4  23929  minveclem3b  24030  ivthlem2  24054  ivthlem3  24055  mbfmax  24251  mbfposr  24254  i1fd  24283  mbfi1fseqlem4  24320  itg2splitlem  24350  itg2monolem1  24352  itg2cnlem1  24363  dvne0  24612  lhop1lem  24614  deg1nn0clb  24689  dgrle  24838  coemulhi  24849  aaliou3lem9  24944  cos11  25123  logleb  25192  argrege0  25200  logdivle  25211  ellogdm  25228  cxple  25284  cxplt2  25287  cxple3  25290  isosctrlem1  25402  atandm  25460  atans2  25515  atantayl2  25522  eldmgm  25605  ftalem7  25662  isppw2  25698  musum  25774  dchrsum2  25850  bposlem1  25866  lgsmod  25905  lgsdir2lem2  25908  lgsdir2  25912  lgsne0  25917  lgsprme0  25921  gausslemma2dlem4  25951  lgsquadlem1  25962  2lgslem3  25986  2lgsoddprm  25998  2sq2  26015  addsqrexnreu  26024  rpvmasumlem  26069  padicabv  26212  ostth3  26220  ostth  26221  istrkgld  26251  axtgupdim2  26263  tglowdim2l  26442  axlowdimlem16  26749  axlowdim2  26752  axlowdim  26753  numedglnl  26935  usgredg2v  27015  lfuhgr1v0e  27042  cusgrfi  27246  vtxd0nedgb  27276  vtxduhgr0edgnel  27282  1loopgrnb0  27290  1hevtxdg0  27293  vtxdgoddnumeven  27341  wlkp1lem1  27461  wlkp1lem2  27462  wlkp1lem5  27465  crctcsh  27608  clwlkclwwlklem2a4  27780  eupth2eucrct  28000  eupth2lem3lem3  28013  eupth2lem3lem4  28014  eupth2lem3lem6  28016  eupth2lem3lem7  28017  eupth2lems  28021  eupth2  28022  konigsberglem4  28038  nfrgr2v  28055  frgrwopreglem3  28097  fusgr2wsp2nb  28117  frgrreggt1  28176  friendshipgt3  28181  lpni  28261  nmobndseqi  28560  minvecolem5  28662  chpsscon3  29284  chnle  29295  nonbooli  29432  pjnel  29507  specval  29679  nmcfnlbi  29833  stri  30038  hstri  30046  cvbr  30063  cvcon3  30065  chcv1  30136  cvexchlem  30149  chrelat2  30151  nelun  30279  elpreq  30296  nelpr  30297  ifeqeqx  30303  nfpconfp  30383  isoun  30443  suppss3  30466  xrge0infss  30490  infxrge0gelb  30496  eliccelico  30506  elicoelioo  30507  nndiffz1  30515  hashgt1  30536  nn0min  30542  toslublem  30660  tosglblem  30662  pmtrcnel  30760  cycpmco2  30802  isarchi2  30841  archiabl  30854  0nellinds  30962  lindssn  30967  lindfpropd  30970  ssmxidl  31009  lbslsat  31044  lindsunlem  31050  ordtcnvNEW  31190  ordtrestNEW  31191  ordtrest2NEWlem  31192  ordtrest2NEW  31193  ordtconnlem1  31194  xrge0iifcnv  31203  esumpcvgval  31364  esum2d  31379  ddemeas  31522  omssubadd  31585  oddpwdc  31639  eulerpartlems  31645  eulerpartlemf  31655  eulerpartlemt  31656  eulerpartlemr  31659  eulerpartlemgvv  31661  eulerpartlemn  31666  ballotlemfc0  31777  ballotlemfcc  31778  ballotlem4  31783  ballotlemimin  31790  ballotlem7  31820  plymulx  31845  signsply0  31848  reprinfz1  31920  reprpmtf1o  31924  reprdifc  31925  hgt750lema  31955  hgt750leme  31956  istrkg2d  31964  bnj23  32015  bnj1185  32092  bnj1228  32310  bnj1388  32332  bnj1417  32340  hashfundm  32381  revwlk  32398  isacycgr  32419  acycgr0v  32422  prclisacycgr  32425  erdszelem10  32474  satf0n0  32652  fmlaomn0  32664  fmlasucdisj  32673  satfv1fvfmla1  32697  satefvfmla1  32699  ismfs  32823  mvtinf  32829  untelirr  32961  untsucf  32963  untangtr  32967  ceqsralv2  32983  dfpo2  33018  dfon2lem3  33057  dfon2lem4  33058  dfon2lem7  33061  dfon2lem9  33063  distel  33075  frpomin  33105  soseq  33123  noextenddif  33202  nodenselem4  33218  nodenselem5  33219  nodenselem7  33221  nolt02o  33226  noresle  33227  noprefixmo  33229  nosupdm  33231  nosupfv  33233  nosupres  33234  nosupbnd1lem1  33235  nosupbnd1lem3  33237  nosupbnd1lem5  33239  nosupbnd1  33241  nosupbnd2lem1  33242  nosupbnd2  33243  slenlt  33258  nocvxminlem  33274  slerec  33304  funpartfv  33433  dfrdg4  33439  nn0prpwlem  33697  nn0prpw  33698  limsucncmpi  33820  limsucncmp  33821  ordcmp  33822  unblimceq0  33873  unbdqndv1  33874  bj-hbntbi  34065  bj-cbvexdv  34151  bj-dtru  34168  bj-ru0  34291  bj-nuliota  34388  topdifinffinlem  34678  topdifinffin  34679  icorempo  34682  relowlpssretop  34695  finxpreclem2  34721  finxpreclem6  34727  wl-ax11-lem8  34901  wl-dfrexf  34924  leceifl  34958  lindsadd  34962  lindsenlbs  34964  matunitlindflem1  34965  poimirlem16  34985  poimirlem17  34986  poimirlem18  34987  poimirlem19  34988  poimirlem21  34990  poimirlem23  34992  poimirlem26  34995  poimirlem27  34996  poimirlem28  34997  poimirlem31  35000  poimir  35002  mblfinlem2  35007  mblfinlem3  35008  ismblfin  35010  cnambfre  35017  itg2addnclem  35020  itg2addnclem2  35021  iblabsnclem  35032  ftc1anclem1  35042  areacirc  35062  heibor1lem  35159  heiborlem1  35161  heiborlem6  35166  heiborlem8  35168  heiborlem10  35170  smprngopr  35402  ecin0  35678  ax12inda  36156  riotaclbgBAD  36162  lcvfbr  36228  lcvbr  36229  lsatcv0  36239  l1cvpat  36262  opltcon3b  36412  cvrfval  36476  cvrval  36477  cvrnbtwn  36479  cvrval2  36482  cvrnbtwn2  36483  cvrnbtwn3  36484  cvrcon3b  36485  cvrnbtwn4  36487  atnlt  36521  iscvlat  36531  cvlexch1  36536  hlsuprexch  36589  hlrelat5N  36609  hlrelat2  36611  cvrval5  36623  3dimlem1  36666  3dim1lem5  36674  3dim2  36676  3dim3  36677  llnnlt  36731  islpln5  36743  lplni2  36745  lvolex3N  36746  lplnnle2at  36749  islpln2a  36756  lplnribN  36759  lplnexllnN  36772  lplnnlt  36773  lvoli3  36785  islvol5  36787  lvoli2  36789  lvolnle3at  36790  islvol2aN  36800  4atlem11  36817  lvolnltN  36826  dalawlem15  37093  4atexlemex2  37279  4atex  37284  4atex2-0aOLDN  37286  4atex2-0cOLDN  37288  lautcvr  37300  ltrnfset  37325  ltrnset  37326  ltrnu  37329  trlfset  37368  trlset  37369  trlval2  37371  cdlemd6  37411  cdleme0nex  37498  cdleme18d  37503  cdleme25b  37562  cdleme25cv  37566  cdleme29b  37583  cdleme31fv  37598  cdleme31fv2  37601  cdlemefrs29bpre0  37604  cdlemefr32sn2aw  37612  cdlemefr29bpre0N  37614  cdlemefr29clN  37615  cdlemefr32fvaN  37617  cdlemefr32fva1  37618  cdlemefs32sn1aw  37622  cdleme32fva  37645  cdleme32fvaw  37647  cdleme40v  37677  cdleme42b  37686  cdleme46f2g2  37701  cdleme46f2g1  37702  cdleme48gfv  37745  cdlemg1fvawlemN  37781  cdlemg1cex  37796  cdlemg6d  37829  cdlemm10N  38326  dicffval  38382  dicfval  38383  dicval  38384  dicfnN  38391  dicvalrelN  38393  dihffval  38438  dihfval  38439  dihlsscpre  38442  dvh4dimat  38646  dvh3dimatN  38647  dvh4dimlem  38651  dvh3dim  38654  dvh4dimN  38655  dvh3dim2  38656  dvh3dim3N  38657  mapdcv  38868  mapdh9aOLDN  38998  hdmapfval  39035  hdmapval  39036  hdmapval2  39040  hdmap11lem2  39050  oexpreposd  39361  ellz1  39564  rencldnfilem  39617  jm2.22  39792  jm2.23  39793  wepwsolem  39842  fnwe2lem2  39851  aomclem8  39861  unxpwdom3  39895  ifpbi12  40052  dfsucon  40087  sqrtcvallem1  40187  ss2iundf  40216  frege124d  40318  clsk3nimkb  40602  clsk1indlem1  40607  clsk1independent  40608  ntrneineine1lem  40646  ntrneicls11  40652  clsneiel1  40670  clsneiel2  40671  neicvgel1  40681  neicvgel2  40682  radcnvrat  40878  rusbcALT  41003  en3lpVD  41411  eliin2f  41602  nssd  41603  wessf1ornlem  41676  limsupre2lem  42232  icccncfext  42395  stoweidlem14  42522  stoweidlem34  42542  stoweidlem59  42567  etransclem24  42766  nnfoctbdjlem  42960  nnfoctbdj  42961  hspmbllem2  43132  nsssmfmbflem  43277  eu2ndop1stv  43547  afvfv0bi  43574  afvco2  43598  ndmaovg  43606  ndfatafv2nrn  43643  afv2ndefb  43646  afv2fv0  43687  nelbr  43696  otiunsndisjX  43701  fun2dmnopgexmpl  43706  ltnltne  43722  readdcnnred  43726  resubcnnred  43727  recnmulnred  43728  cndivrenred  43729  ichnreuop  43855  fmtnoinf  43919  odz2prm2pw  43946  prmdvdsfmtnof1lem2  43968  lighneallem3  43991  lighneallem4  43994  requad1  44006  isodd3  44036  bits0ALTV  44063  nfermltl8rev  44126  nfermltl2rev  44127  nfermltlrev  44128  lidldomnnring  44420  zrninitoringc  44561  ztprmneprm  44614  lindepsnlininds  44726  islindeps  44727  lindslinindsimp2lem5  44736  lindslinindsimp2  44737  difmodm1lt  44801  line2ylem  45019  line2xlem  45021  elsetrecslem  45082
  Copyright terms: Public domain W3C validator