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  1919  hba1w  1923  hbe1w  1924  cbvexv1  2116  cbvex  2163  cbvexv  2166  cbvexd  2169  cbvex2  2171  cbvexdva  2174  drex1  2219  eujustALT  2365  necon3abid  2722  neleq12d  2791  cbvrexf  3046  gencbval  3129  spcegf  3166  spc2gv  3173  spc3gv  3175  cdeqnot  3294  ru  3305  sbcng  3347  sbcrext  3382  sbcrextOLD  3383  cbvrexcsf  3436  difjust  3446  eldif  3454  dfpss3  3559  difeq2  3588  disjne  3877  pssdifcom1  3909  eldifpr  4055  elpwunsn  4074  eldiftp  4078  prel12  4222  prel12g  4226  disjxun  4479  nalset  4622  pwnss  4655  dtru  4682  rexxfrd  4706  rexxfr2d  4708  rexxfrd2  4710  rexxfr  4713  dtruALT  4725  dtruALT2  4737  opthneg  4774  otiunsndisj  4800  poeq1  4856  pocl  4860  swopo  4863  sotric  4879  sotrieq  4880  isso2i  4885  somo  4887  freq1  4902  frirr  4909  fr2nr  4910  frminex  4912  tz7.2  4916  wereu2  4929  poinxp  4999  frinxp  5001  posn  5004  frsn  5006  rexiunxp  5076  rexxpf  5083  intirr  5324  poirr2  5330  cnvpo  5480  predpoirr  5515  predfrirr  5516  nordeq  5549  ordtri1  5563  ordtri3  5566  ordtri3OLD  5567  fvmpti  6079  fndmdif  6118  rexrnmpt  6166  f1imapss  6306  cbvexfo  6327  soisoi  6360  isopolem  6377  weniso  6386  canth  6390  riotaclb  6430  rexrnmpt2  6556  ndmovg  6596  sorpssuni  6725  sorpssint  6726  fr3nr  6752  dfwe2  6754  ordsucsssuc  6796  nlimsucg  6815  orduninsuc  6816  dfom2  6840  ssnlim  6856  f1oweALT  6923  frxp  7054  poxp  7056  wfrlem10  7191  smoword  7230  tz7.48lem  7303  oacan  7395  oaword  7396  omlimcl  7425  omeulem1  7429  nnaword  7474  nnmword  7480  nneob  7499  brdifun  7538  swoer  7539  undifixp  7710  boxcutc  7717  2dom  7795  php  7909  nndomo  7919  nnsdomo  7920  unxpdomlem2  7930  frfi  7970  unfilem1  7989  supeq3  8118  supeq123d  8119  supmo  8121  eqsup  8125  supub  8128  sup0  8135  suppr  8140  supisolem  8142  supisoex  8143  eqinf  8153  infval  8155  infmo  8164  infpr  8172  infempty  8175  oieq1  8180  ordtypecbv  8185  ordtypelem7  8192  wemapsolem  8218  canthwdom  8247  zfregcl  8262  zfregclOLD  8264  elirrv  8267  elirr  8268  noinfep  8320  cantnfp1lem3  8340  rankr1clem  8446  carden2b  8556  domtri2  8578  alephord3  8664  alephdom2  8673  alephval3  8696  dfac9  8721  kmlem2  8736  kmlem4  8738  isfin4  8882  isfin7  8886  fin23lem11  8902  isf32lem5  8942  isf34lem4  8962  fin1a2lem6  8990  fin1a2lem7  8991  fin1a2lem12  8996  itunisuc  9004  ac6n  9070  zorn2g  9088  zornn0g  9090  ttukeylem7  9100  axpowndlem3  9180  axpowndlem4  9181  axregnd  9185  elgch  9203  engch  9209  fpwwe2lem13  9223  fpwwe2  9224  pwfseqlem1  9239  pwfseqlem3  9241  hargch  9254  addnidpi  9482  pinq  9508  nqereu  9510  ltsonq  9550  prlem934  9614  ltexprlem7  9623  addcanpr  9627  prlem936  9628  reclem2pr  9629  reclem3pr  9630  supexpr  9635  ltsosr  9674  supsrlem  9691  axpre-lttri  9745  axpre-sup  9749  xrlenlt  9857  axlttri  9863  axsup  9867  ltne  9888  dedekind  9955  readdcan  9965  leadd1  10249  ltsub1  10277  ltsub2  10278  leord1  10308  lediv1  10641  lemuldiv  10657  lerec  10660  le2msq  10677  lbinf  10730  lbinfmOLD  10731  infm3  10739  suprnub  10743  infregelb  10764  infmrgelbOLD  10765  infmrlbOLD  10767  avgle1  11031  avgle2  11032  znnnlt1  11149  indstr  11500  zsupss  11523  uzsupss  11526  rpneg  11609  xralrple  11783  xleneg  11796  xltadd1  11829  xposdif  11835  xmulneg1  11842  xltmul1  11865  xrsupexmnf  11877  xrinfmexpnf  11878  xrsupsslem  11879  xrinfmsslem  11880  xrub  11884  supxrleub  11899  infxrgelb  11908  infmxrgelbOLD  11912  difreicc  12048  nn0disj  12196  nelfzo  12216  elfznelfzo  12311  fvinim0ffz  12321  injresinjlem  12322  ssnn0fi  12518  leexp2  12649  hashbnd  12857  hasheni  12867  hashbc  12963  wrdsymb0  13057  swrdnd  13147  swrdnd2  13148  repswswrd  13245  repswccat  13246  cshwidxmod  13263  cnpart  13691  sqrtlt  13713  limsuplt  13926  rlimrege0  14028  isercoll  14116  efle  14560  odd2np1  14776  sumodd  14822  divalglem7  14835  ndvdsadd  14848  fldivndvdslt  14852  bitsfval  14859  bitsval  14860  bits0  14864  bitsp1  14867  bitsmod  14873  bitscmp  14875  bitsinv1lem  14878  sadadd2lem2  14887  saddisjlem  14901  bitsshft  14912  gcdneg  14958  algcvgblem  15008  lcmneg  15034  isprm3  15114  dvdsnprmd  15121  isprm5  15137  rpexp  15150  phiprmpw  15201  m1dvdsndvds  15229  pythagtrip  15265  pcgcd1  15307  prmpwdvds  15334  prmreclem2  15347  prmreclem3  15348  prmreclem5  15350  prmreclem6  15351  vdwlem6  15416  vdwnnlem2  15426  vdwnnlem3  15427  vdwnn  15428  prmo1  15467  prmlem0  15538  prmlem1a  15539  divsfval  15926  mrisval  16009  ismri  16010  ismri2dad  16016  cidpropd  16089  plttr  16689  joinval  16724  meetval  16738  acsfiindd  16896  isnsgrp  17007  mgm2nsgrplem2  17125  sgrp2nmndlem3  17131  symgfix2  17555  pmtrdifellem4  17618  psgnunilem1  17632  psgnunilem5  17633  psgnunilem2  17634  psgnunilem3  17635  pmtrsn  17658  sylow1lem3  17750  sylow2alem2  17768  efgsfo  17887  ablfac1eulem  18205  ablfac1eu  18206  pgpfac1lem1  18207  pgpfac1lem5  18212  islbs  18805  lbsind  18809  lbspss  18811  lbspropd  18828  lspsnne1  18846  islbs2  18883  lbsacsbs  18885  lbsextlem1  18887  lbsextlem3  18889  lbsextlem4  18890  lbsextg  18891  nzrunit  18996  opsrtoslem2  19214  cply1coe0  19398  cply1coe0bi  19399  frlmlbs  19862  islindf  19877  islinds2  19878  islindf2  19879  lindfind  19881  lindsind  19882  lindfrn  19886  lindfmm  19892  lsslindf  19895  islindf4  19903  mdetunilem7  20150  mdetunilem8  20151  mdetunilem9  20152  maducoeval2  20172  pmatcollpw3fi1lem1  20317  fvmptnn04ifa  20381  fvmptnn04ifc  20383  fvmptnn04ifd  20384  chfacffsupp  20387  chfacfscmul0  20389  chfacfpmmul0  20393  elcls  20594  maxlp  20668  perfi  20676  ordtbaslem  20709  ordtval  20710  ordtbas2  20712  ordtopn1  20715  ordtopn2  20716  ordtcnv  20722  ordtrest  20723  ordtrest2lem  20724  ordtrest2  20725  pnfnei  20741  mnfnei  20742  isreg2  20898  ordthauslem  20904  cmpfi  20928  cmpfii  20929  bwth  20930  nconsubb  20943  hausdiag  21165  txkgen  21172  kqdisj  21252  ordthmeolem  21321  fbfinnfr  21362  trfbas  21365  fbunfip  21390  fbasrn  21405  trfil3  21409  ufileu  21440  fin1aufil  21453  hausflim  21502  alexsubALTlem2  21569  alexsubALTlem3  21570  alexsubALTlem4  21571  ptcmplem2  21574  ptcmplem3  21575  stdbdbl  22038  iccntr  22345  reconnlem2  22351  iccpnfcnv  22478  xrhmeo  22480  lebnumlem1  22495  lebnumlem2  22496  lebnumlem3  22497  bcthlem4  22799  minveclem3b  22874  minveclem3bOLD  22886  ivthlem2  22907  ivthlem3  22908  mbfmax  23101  mbfposr  23104  i1fd  23133  mbfi1fseqlem4  23170  itg2splitlem  23200  itg2monolem1  23202  itg2cnlem1  23213  dvne0  23457  lhop1lem  23459  deg1nn0clb  23533  dgrle  23691  coemulhi  23702  aaliou3lem9  23800  cos11  23974  logleb  24044  argrege0  24052  logdivle  24063  ellogdm  24076  cxple  24132  cxplt2  24135  cxple3  24138  isosctrlem1  24239  atandm  24294  atans2  24349  atantayl2  24356  eldmgm  24439  ftalem7  24498  isppw2  24534  musum  24610  dchrsum2  24686  bposlem1  24702  lgsmod  24741  lgsdir2lem2  24744  lgsdir2  24748  lgsne0  24753  lgsprme0  24757  gausslemma2dlem4  24787  lgsquadlem1  24798  2lgslem3  24822  2lgsoddprm  24834  rpvmasumlem  24869  padicabv  25012  ostth3  25020  ostth  25021  istrkgld  25051  axtgupdim2  25063  tglowdim2l  25239  axlowdimlem16  25531  axlowdim2  25534  axlowdim  25535  usgra1v  25661  usgraidx2v  25664  nbgra0nb  25700  cusgrafilem3  25751  spthispth  25845  wlkdvspthlem  25879  clwlkisclwwlklem2a4  26054  clwlknclwlkdifs  26229  eupath2lem3  26248  eupath2  26249  konigsberg  26256  frgra2v  26268  frgrancvvdeqlem2  26300  2spotiundisj  26331  usg2spot2nb  26334  2spotmdisj  26337  frgrareggt1  26385  friendshipgt3  26390  lpni  26464  nmobndseqi  26800  minvecolem5  26903  minvecolem5OLD  26913  chpsscon3  27538  chnle  27549  nonbooli  27686  pjnel  27761  specval  27933  nmcfnlbi  28087  stri  28292  hstri  28300  cvbr  28317  cvcon3  28319  chcv1  28390  cvexchlem  28403  chrelat2  28405  spc2d  28489  elpreq  28536  ifeqeqx  28537  isoun  28654  suppss3  28682  xrge0infss  28709  xrge0infssOLD  28710  xrge0infssdOLD  28712  infxrge0lbOLD  28716  infxrge0gelb  28719  infxrge0gelbOLD  28720  eliccelico  28728  elicoelioo  28729  nndiffz1  28735  nn0min  28753  toslublem  28797  tosglblem  28799  isarchi2  28870  archiabl  28883  ordtcnvNEW  29094  ordtrestNEW  29095  ordtrest2NEWlem  29096  ordtrest2NEW  29097  ordtconlem1  29098  xrge0iifcnv  29107  elzdif0  29152  esumpcvgval  29267  esum2d  29282  ddemeas  29426  omssubadd  29495  oms0OLD  29496  omssubaddOLD  29499  oddpwdc  29554  eulerpartlems  29560  eulerpartlemf  29570  eulerpartlemt  29571  eulerpartlemr  29574  eulerpartlemgvv  29576  eulerpartlemn  29581  ballotlemfc0  29692  ballotlemfcc  29693  ballotlem4  29698  ballotlemimin  29705  ballotlem7  29735  ballotlemiminOLD  29743  ballotlem7OLD  29773  plymulx  29800  signsply0  29803  istrkg2d  29846  bnj23  29887  bnj1185  29967  bnj1228  30182  bnj1388  30204  bnj1417  30212  erdszelem10  30285  ismfs  30549  mvtinf  30555  untelirr  30686  untsucf  30688  untangtr  30692  ceqsralv2  30709  inffz  30714  dfpo2  30744  dfon2lem3  30780  dfon2lem4  30781  dfon2lem7  30784  dfon2lem9  30786  distel  30799  soseq  30841  nodenselem4  30922  nodenselem5  30923  nocvxminlem  30928  nofulllem4  30943  funpartfv  31061  dfrdg4  31067  nn0prpwlem  31325  nn0prpw  31326  limsucncmpi  31452  limsucncmp  31453  ordcmp  31454  unblimceq0  31506  unbdqndv1  31507  bj-hbntbi  31720  bj-cbvexdv  31761  bj-cbvex2v  31763  bj-drex1v  31776  bj-nalset  31827  bj-dtru  31830  bj-ru0  31959  bj-nuliota  32045  topdifinffinlem  32206  topdifinffin  32207  icorempt2  32210  relowlpssretop  32223  finxpreclem2  32238  finxpreclem6  32244  wl-ax11-lem8  32442  leceifl  32462  lindsenlbs  32468  matunitlindflem1  32469  poimirlem16  32489  poimirlem17  32490  poimirlem18  32491  poimirlem19  32492  poimirlem21  32494  poimirlem23  32496  poimirlem26  32499  poimirlem27  32500  poimirlem28  32501  poimirlem31  32504  poimir  32506  mblfinlem2  32511  mblfinlem3  32512  ismblfin  32514  cnambfre  32522  itg2addnclem  32525  itg2addnclem2  32526  iblabsnclem  32537  ftc1anclem1  32549  areacirc  32569  heibor1lem  32672  heiborlem1  32674  heiborlem6  32679  heiborlem8  32681  heiborlem10  32683  smprngopr  32915  ax12inda  33145  riotaclbgBAD  33152  lcvfbr  33219  lcvbr  33220  lsatcv0  33230  l1cvpat  33253  opltcon3b  33403  cvrfval  33467  cvrval  33468  cvrnbtwn  33470  cvrval2  33473  cvrnbtwn2  33474  cvrnbtwn3  33475  cvrcon3b  33476  cvrnbtwn4  33478  atnlt  33512  iscvlat  33522  cvlexch1  33527  hlsuprexch  33579  hlrelat5N  33599  hlrelat2  33601  cvrval5  33613  3dimlem1  33656  3dim1lem5  33664  3dim2  33666  3dim3  33667  llnnlt  33721  islpln5  33733  lplni2  33735  lvolex3N  33736  lplnnle2at  33739  islpln2a  33746  lplnribN  33749  lplnexllnN  33762  lplnnlt  33763  lvoli3  33775  islvol5  33777  lvoli2  33779  lvolnle3at  33780  islvol2aN  33790  4atlem11  33807  lvolnltN  33816  dalawlem15  34083  4atexlemex2  34269  4atex  34274  4atex2-0aOLDN  34276  4atex2-0cOLDN  34278  lautcvr  34290  ltrnfset  34315  ltrnset  34316  ltrnu  34319  trlfset  34359  trlset  34360  trlval2  34362  cdlemd6  34402  cdleme0nex  34489  cdleme18d  34494  cdleme25b  34554  cdleme25cv  34558  cdleme29b  34575  cdleme31fv  34590  cdleme31fv2  34593  cdlemefrs29bpre0  34596  cdlemefr32sn2aw  34604  cdlemefr29bpre0N  34606  cdlemefr29clN  34607  cdlemefr32fvaN  34609  cdlemefr32fva1  34610  cdlemefs32sn1aw  34614  cdleme32fva  34637  cdleme32fvaw  34639  cdleme40v  34669  cdleme42b  34678  cdleme46f2g2  34693  cdleme46f2g1  34694  cdleme48gfv  34737  cdlemg1fvawlemN  34773  cdlemg1cex  34788  cdlemg6d  34821  cdlemm10N  35319  dicffval  35375  dicfval  35376  dicval  35377  dicfnN  35384  dicvalrelN  35386  dihffval  35431  dihfval  35432  dihlsscpre  35435  dvh4dimat  35639  dvh3dimatN  35640  dvh4dimlem  35644  dvh3dim  35647  dvh4dimN  35648  dvh3dim2  35649  dvh3dim3N  35650  mapdcv  35861  mapdh9aOLDN  35992  hdmapfval  36031  hdmapval  36032  hdmapval2  36036  hdmap11lem2  36046  ellz1  36242  rencldnfilem  36296  jm2.22  36474  jm2.23  36475  wepwsolem  36524  fnwe2lem2  36533  aomclem8  36543  unxpwdom3  36577  ifpbi12  36753  ifpbi123  36755  relintabex  36807  ss2iundf  36871  frege124d  36973  clsk3nimkb  37259  clsk1indlem1  37264  clsk1independent  37265  ntrneineine1lem  37303  ntrneicls11  37309  clsneiel1  37327  clsneiel2  37328  neicvgel1  37338  neicvgel2  37339  radcnvrat  37436  rusbcALT  37563  en3lpVD  38003  eliin2f  38218  nssd  38219  wessf1ornlem  38268  icccncfext  38677  stoweidlem14  38814  stoweidlem34  38834  stoweidlem59  38859  etransclem24  39061  nnfoctbdjlem  39259  nnfoctbdj  39260  hspmbllem2  39428  smfmbfcex  39557  nsssmfmbflem  39575  eu2ndop1stv  39762  afvfv0bi  39793  afvco2  39817  ndmaovg  39825  fmtnoinf  39898  odz2prm2pw  39925  prmdvdsfmtnof1lem2  39947  lighneallem3  39974  lighneallem4  39977  isodd3  40015  bits0ALTV  40040  otiunsndisjX  40239  2f1fvneq  40245  fun2dmnopgexmpl  40263  ltnltne  40279  usgredg2v  40563  lfuhgr1v0e  40589  cusgrfi  40783  vtxd0nedgb  40812  vtxduhgr0edgnel  40818  1loopgrnb0  40826  1hevtxdg0  40829  1wlkp1lem1  40991  1wlkp1lem2  40992  1wlkp1lem5  40995  crctcsh  41136  clwwlknclwwlkdifs  41290  clwlkclwwlklem2a4  41315  eupth2eucrct  41494  eupth2lem3lem3  41507  eupth2lem3lem4  41508  eupth2lem3lem6  41510  eupth2lem3lem7  41511  eupth2lems  41515  eupth2  41516  konigsberglem4  41534  nfrgr2v  41551  frgrncvvdeqlem2  41579  fusgr2wsp2nb  41607  av-frgrareggt1  41656  av-friendshipgt3  41661  lidldomnnring  41829  zrninitoringc  41972  ztprmneprm  42027  lindepsnlininds  42144  islindeps  42145  lindslinindsimp2lem5  42154  lindslinindsimp2  42155  difmodm1lt  42220
  Copyright terms: Public domain W3C validator