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

Theorem notbid 308
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 304 . . 3 (𝜓 ↔ ¬ ¬ 𝜓)
3 notnotb 304 . . 3 (𝜒 ↔ ¬ ¬ 𝜒)
41, 2, 33bitr3g 302 . 2 (𝜑 → (¬ ¬ 𝜓 ↔ ¬ ¬ 𝜒))
54con4bid 307 1 (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196
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 197
This theorem is referenced by:  notbi  309  ifpbi123d  1026  con3ALT  1031  con3OLD  1034  nanbi1  1452  xorbi12d  1475  cbvexvw  1972  hba1wOLD  1977  hbe1w  1978  cbvexv1  2180  cbvex  2276  cbvexv  2279  cbvexd  2282  cbvex2  2284  cbvexdva  2287  drex1  2331  eujustALT  2477  necon3abid  2832  neleq12d  2903  cbvrexf  3159  gencbval  3243  spcegf  3280  spc2gv  3287  spc3gv  3289  cdeqnot  3410  ru  3421  sbcng  3463  sbcrext  3498  sbcrextOLD  3499  cbvrexcsf  3552  difjust  3562  eldif  3570  dfpss3  3676  difeq2  3705  disjne  3999  pssdifcom1  4031  eldifpr  4180  elpwunsn  4200  eldiftp  4204  prel12  4356  prel12g  4360  disjxun  4616  nalset  4760  pwnss  4795  dtru  4822  rexxfrd  4846  rexxfr2d  4848  rexxfrd2  4850  rexxfr  4853  dtruALT  4865  dtruALT2  4877  opthneg  4915  otiunsndisj  4945  poeq1  5003  pocl  5007  swopo  5010  sotric  5026  sotrieq  5027  isso2i  5032  somo  5034  freq1  5049  frirr  5056  fr2nr  5057  frminex  5059  tz7.2  5063  wereu2  5076  poinxp  5148  frinxp  5150  posn  5153  frsn  5155  rexiunxp  5227  rexxpf  5234  intirr  5477  poirr2  5483  cnvpo  5635  predpoirr  5670  predfrirr  5671  nordeq  5704  ordtri1  5718  ordtri3  5721  ordtri3OLD  5722  fvmpti  6239  fndmdif  6278  rexrnmpt  6326  2f1fvneq  6472  f1imapss  6478  cbvexfo  6500  soisoi  6533  isopolem  6550  weniso  6559  canth  6563  riotaclb  6604  rexrnmpt2  6730  ndmovg  6771  sorpssuni  6900  sorpssint  6901  fr3nr  6927  dfwe2  6929  ordsucsssuc  6971  nlimsucg  6990  orduninsuc  6991  dfom2  7015  ssnlim  7031  f1oweALT  7100  frxp  7233  poxp  7235  wfrlem10  7370  smoword  7409  tz7.48lem  7482  oacan  7574  oaword  7575  omlimcl  7604  omeulem1  7608  nnaword  7653  nnmword  7659  nneob  7678  brdifun  7717  swoer  7718  undifixp  7889  boxcutc  7896  2dom  7974  php  8089  nndomo  8099  nnsdomo  8100  unxpdomlem2  8110  frfi  8150  unfilem1  8169  supeq3  8300  supeq123d  8301  supmo  8303  eqsup  8307  supub  8310  sup0  8317  suppr  8322  supisolem  8324  supisoex  8325  eqinf  8335  infval  8337  infmo  8346  infpr  8354  infempty  8357  oieq1  8362  ordtypecbv  8367  ordtypelem7  8374  wemapsolem  8400  canthwdom  8429  zfregcl  8444  zfregclOLD  8446  elirrv  8449  elirr  8450  noinfep  8502  cantnfp1lem3  8522  rankr1clem  8628  carden2b  8738  domtri2  8760  alephord3  8846  alephdom2  8855  alephval3  8878  dfac9  8903  kmlem2  8918  kmlem4  8920  isfin4  9064  isfin7  9068  fin23lem11  9084  isf32lem5  9124  isf34lem4  9144  fin1a2lem6  9172  fin1a2lem7  9173  fin1a2lem12  9178  itunisuc  9186  ac6n  9252  zorn2g  9270  zornn0g  9272  ttukeylem7  9282  axpowndlem3  9366  axpowndlem4  9367  axregnd  9371  elgch  9389  engch  9395  fpwwe2lem13  9409  fpwwe2  9410  pwfseqlem1  9425  pwfseqlem3  9427  hargch  9440  addnidpi  9668  pinq  9694  nqereu  9696  ltsonq  9736  prlem934  9800  ltexprlem7  9809  addcanpr  9813  prlem936  9814  reclem2pr  9815  reclem3pr  9816  supexpr  9821  ltsosr  9860  supsrlem  9877  axpre-lttri  9931  axpre-sup  9935  xrlenlt  10048  axlttri  10054  axsup  10058  ltne  10079  dedekind  10145  readdcan  10155  leadd1  10441  ltsub1  10469  ltsub2  10470  leord1  10500  lediv1  10833  lemuldiv  10848  lerec  10851  le2msq  10868  lbinf  10921  infm3  10927  suprnub  10933  infregelb  10952  avgle1  11217  avgle2  11218  znnnlt1  11349  indstr  11700  zsupss  11721  uzsupss  11724  rpneg  11807  xralrple  11978  xleneg  11991  xltadd1  12026  xposdif  12032  xmulneg1  12039  xltmul1  12062  xrsupexmnf  12075  xrinfmexpnf  12076  xrsupsslem  12077  xrinfmsslem  12078  xrub  12082  supxrleub  12096  infxrgelb  12105  difreicc  12243  nn0disj  12393  nelfzo  12413  elfznelfzo  12511  fvinim0ffz  12524  injresinjlem  12525  ssnn0fi  12721  leexp2  12852  hashbnd  13060  hasheni  13073  hashbc  13172  wrdsymb0  13273  swrdnd  13365  swrdnd2  13366  repswswrd  13463  repswccat  13464  cshwidxmod  13481  cnpart  13909  sqrtlt  13931  limsuplt  14139  rlimrege0  14239  isercoll  14327  efle  14768  odd2np1  14984  sumodd  15030  divalglem7  15041  ndvdsadd  15053  fldivndvdslt  15057  bitsfval  15064  bitsval  15065  bits0  15069  bitsp1  15072  bitsmod  15077  bitscmp  15079  bitsinv1lem  15082  sadadd2lem2  15091  saddisjlem  15105  bitsshft  15116  gcdneg  15162  algcvgblem  15209  lcmneg  15235  isprm3  15315  dvdsnprmd  15322  isprm5  15338  rpexp  15351  phiprmpw  15400  m1dvdsndvds  15422  pythagtrip  15458  pcgcd1  15500  prmpwdvds  15527  prmreclem2  15540  prmreclem3  15541  prmreclem5  15543  prmreclem6  15544  vdwlem6  15609  vdwnnlem2  15619  vdwnnlem3  15620  vdwnn  15621  prmo1  15660  prmlem0  15731  prmlem1a  15732  divsfval  16123  mrisval  16206  ismri  16207  ismri2dad  16213  cidpropd  16286  plttr  16886  joinval  16921  meetval  16935  acsfiindd  17093  isnsgrp  17204  mgm2nsgrplem2  17322  sgrp2nmndlem3  17328  symgfix2  17752  pmtrdifellem4  17815  psgnunilem1  17829  psgnunilem5  17830  psgnunilem2  17831  psgnunilem3  17832  pmtrsn  17855  sylow1lem3  17931  sylow2alem2  17949  efgsfo  18068  ablfac1eulem  18387  ablfac1eu  18388  pgpfac1lem1  18389  pgpfac1lem5  18394  islbs  18990  lbsind  18994  lbspss  18996  lbspropd  19013  lspsnne1  19031  islbs2  19068  lbsacsbs  19070  lbsextlem1  19072  lbsextlem3  19074  lbsextlem4  19075  lbsextg  19076  nzrunit  19181  opsrtoslem2  19399  cply1coe0  19583  cply1coe0bi  19584  frlmlbs  20050  islindf  20065  islinds2  20066  islindf2  20067  lindfind  20069  lindsind  20070  lindfrn  20074  lindfmm  20080  lsslindf  20083  islindf4  20091  mdetunilem7  20338  mdetunilem8  20339  mdetunilem9  20340  maducoeval2  20360  pmatcollpw3fi1lem1  20505  fvmptnn04ifa  20569  fvmptnn04ifc  20571  fvmptnn04ifd  20572  chfacffsupp  20575  chfacfscmul0  20577  chfacfpmmul0  20581  elcls  20782  maxlp  20856  perfi  20864  ordtbaslem  20897  ordtval  20898  ordtbas2  20900  ordtopn1  20903  ordtopn2  20904  ordtcnv  20910  ordtrest  20911  ordtrest2lem  20912  ordtrest2  20913  pnfnei  20929  mnfnei  20930  isreg2  21086  ordthauslem  21092  cmpfi  21116  cmpfii  21117  bwth  21118  nconnsubb  21131  hausdiag  21353  txkgen  21360  kqdisj  21440  ordthmeolem  21509  fbfinnfr  21550  trfbas  21553  fbunfip  21578  fbasrn  21593  trfil3  21597  ufileu  21628  fin1aufil  21641  hausflim  21690  alexsubALTlem2  21757  alexsubALTlem3  21758  alexsubALTlem4  21759  ptcmplem2  21762  ptcmplem3  21763  stdbdbl  22227  iccntr  22527  reconnlem2  22533  iccpnfcnv  22646  xrhmeo  22648  lebnumlem1  22663  lebnumlem2  22664  lebnumlem3  22665  bcthlem4  23027  minveclem3b  23102  ivthlem2  23123  ivthlem3  23124  mbfmax  23317  mbfposr  23320  i1fd  23349  mbfi1fseqlem4  23386  itg2splitlem  23416  itg2monolem1  23418  itg2cnlem1  23429  dvne0  23673  lhop1lem  23675  deg1nn0clb  23749  dgrle  23898  coemulhi  23909  aaliou3lem9  24004  cos11  24178  logleb  24248  argrege0  24256  logdivle  24267  ellogdm  24280  cxple  24336  cxplt2  24339  cxple3  24342  isosctrlem1  24443  atandm  24498  atans2  24553  atantayl2  24560  eldmgm  24643  ftalem7  24700  isppw2  24736  musum  24812  dchrsum2  24888  bposlem1  24904  lgsmod  24943  lgsdir2lem2  24946  lgsdir2  24950  lgsne0  24955  lgsprme0  24959  gausslemma2dlem4  24989  lgsquadlem1  25000  2lgslem3  25024  2lgsoddprm  25036  rpvmasumlem  25071  padicabv  25214  ostth3  25222  ostth  25223  istrkgld  25253  axtgupdim2  25265  tglowdim2l  25440  axlowdimlem16  25732  axlowdim2  25735  axlowdim  25736  usgredg2v  26006  lfuhgr1v0e  26033  cusgrfi  26235  vtxd0nedgb  26264  vtxduhgr0edgnel  26270  1loopgrnb0  26278  1hevtxdg0  26281  wlkp1lem1  26433  wlkp1lem2  26434  wlkp1lem5  26437  crctcsh  26579  clwwlknclwwlkdifs  26734  clwlkclwwlklem2a4  26759  eupth2eucrct  26937  eupth2lem3lem3  26950  eupth2lem3lem4  26951  eupth2lem3lem6  26953  eupth2lem3lem7  26954  eupth2lems  26958  eupth2  26959  konigsberglem4  26977  nfrgr2v  26994  frgrncvvdeqlem2  27022  fusgr2wsp2nb  27050  frgrreggt1  27099  friendshipgt3  27104  lpni  27178  nmobndseqi  27474  minvecolem5  27577  chpsscon3  28202  chnle  28213  nonbooli  28350  pjnel  28425  specval  28597  nmcfnlbi  28751  stri  28956  hstri  28964  cvbr  28981  cvcon3  28983  chcv1  29054  cvexchlem  29067  chrelat2  29069  spc2d  29153  elpreq  29198  ifeqeqx  29199  isoun  29313  suppss3  29336  xrge0infss  29361  infxrge0gelb  29367  eliccelico  29375  elicoelioo  29376  nndiffz1  29382  nn0min  29400  toslublem  29444  tosglblem  29446  isarchi2  29516  archiabl  29529  ordtcnvNEW  29740  ordtrestNEW  29741  ordtrest2NEWlem  29742  ordtrest2NEW  29743  ordtconnlem1  29744  xrge0iifcnv  29753  elzdif0  29798  esumpcvgval  29913  esum2d  29928  ddemeas  30072  omssubadd  30135  oddpwdc  30189  eulerpartlems  30195  eulerpartlemf  30205  eulerpartlemt  30206  eulerpartlemr  30209  eulerpartlemgvv  30211  eulerpartlemn  30216  ballotlemfc0  30327  ballotlemfcc  30328  ballotlem4  30333  ballotlemimin  30340  ballotlem7  30370  plymulx  30397  signsply0  30400  istrkg2d  30443  bnj23  30484  bnj1185  30564  bnj1228  30779  bnj1388  30801  bnj1417  30809  erdszelem10  30882  ismfs  31146  mvtinf  31152  untelirr  31285  untsucf  31287  untangtr  31291  ceqsralv2  31308  inffzOLD  31314  dfpo2  31344  dfon2lem3  31379  dfon2lem4  31380  dfon2lem7  31383  dfon2lem9  31385  distel  31398  soseq  31440  nodenselem4  31528  nodenselem5  31529  nocvxminlem  31534  nofulllem4  31549  funpartfv  31667  dfrdg4  31673  nn0prpwlem  31932  nn0prpw  31933  limsucncmpi  32059  limsucncmp  32060  ordcmp  32061  unblimceq0  32113  unbdqndv1  32114  bj-hbntbi  32310  bj-cbvexdv  32351  bj-cbvex2v  32353  bj-drex1v  32365  bj-nalset  32410  bj-dtru  32413  bj-ru0  32552  bj-nuliota  32639  topdifinffinlem  32800  topdifinffin  32801  icorempt2  32804  relowlpssretop  32817  finxpreclem2  32832  finxpreclem6  32838  wl-ax11-lem8  32977  leceifl  32997  lindsenlbs  33003  matunitlindflem1  33004  poimirlem16  33024  poimirlem17  33025  poimirlem18  33026  poimirlem19  33027  poimirlem21  33029  poimirlem23  33031  poimirlem26  33034  poimirlem27  33035  poimirlem28  33036  poimirlem31  33039  poimir  33041  mblfinlem2  33046  mblfinlem3  33047  ismblfin  33049  cnambfre  33057  itg2addnclem  33060  itg2addnclem2  33061  iblabsnclem  33072  ftc1anclem1  33084  areacirc  33104  heibor1lem  33207  heiborlem1  33209  heiborlem6  33214  heiborlem8  33216  heiborlem10  33218  smprngopr  33450  ax12inda  33680  riotaclbgBAD  33687  lcvfbr  33754  lcvbr  33755  lsatcv0  33765  l1cvpat  33788  opltcon3b  33938  cvrfval  34002  cvrval  34003  cvrnbtwn  34005  cvrval2  34008  cvrnbtwn2  34009  cvrnbtwn3  34010  cvrcon3b  34011  cvrnbtwn4  34013  atnlt  34047  iscvlat  34057  cvlexch1  34062  hlsuprexch  34114  hlrelat5N  34134  hlrelat2  34136  cvrval5  34148  3dimlem1  34191  3dim1lem5  34199  3dim2  34201  3dim3  34202  llnnlt  34256  islpln5  34268  lplni2  34270  lvolex3N  34271  lplnnle2at  34274  islpln2a  34281  lplnribN  34284  lplnexllnN  34297  lplnnlt  34298  lvoli3  34310  islvol5  34312  lvoli2  34314  lvolnle3at  34315  islvol2aN  34325  4atlem11  34342  lvolnltN  34351  dalawlem15  34618  4atexlemex2  34804  4atex  34809  4atex2-0aOLDN  34811  4atex2-0cOLDN  34813  lautcvr  34825  ltrnfset  34850  ltrnset  34851  ltrnu  34854  trlfset  34894  trlset  34895  trlval2  34897  cdlemd6  34937  cdleme0nex  35024  cdleme18d  35029  cdleme25b  35089  cdleme25cv  35093  cdleme29b  35110  cdleme31fv  35125  cdleme31fv2  35128  cdlemefrs29bpre0  35131  cdlemefr32sn2aw  35139  cdlemefr29bpre0N  35141  cdlemefr29clN  35142  cdlemefr32fvaN  35144  cdlemefr32fva1  35145  cdlemefs32sn1aw  35149  cdleme32fva  35172  cdleme32fvaw  35174  cdleme40v  35204  cdleme42b  35213  cdleme46f2g2  35228  cdleme46f2g1  35229  cdleme48gfv  35272  cdlemg1fvawlemN  35308  cdlemg1cex  35323  cdlemg6d  35356  cdlemm10N  35854  dicffval  35910  dicfval  35911  dicval  35912  dicfnN  35919  dicvalrelN  35921  dihffval  35966  dihfval  35967  dihlsscpre  35970  dvh4dimat  36174  dvh3dimatN  36175  dvh4dimlem  36179  dvh3dim  36182  dvh4dimN  36183  dvh3dim2  36184  dvh3dim3N  36185  mapdcv  36396  mapdh9aOLDN  36527  hdmapfval  36566  hdmapval  36567  hdmapval2  36571  hdmap11lem2  36581  ellz1  36777  rencldnfilem  36831  jm2.22  37009  jm2.23  37010  wepwsolem  37059  fnwe2lem2  37068  aomclem8  37078  unxpwdom3  37112  ifpbi12  37281  ifpbi123  37283  relintabex  37335  ss2iundf  37399  frege124d  37501  clsk3nimkb  37787  clsk1indlem1  37792  clsk1independent  37793  ntrneineine1lem  37831  ntrneicls11  37837  clsneiel1  37855  clsneiel2  37856  neicvgel1  37866  neicvgel2  37867  radcnvrat  37962  rusbcALT  38089  en3lpVD  38530  eliin2f  38739  nssd  38740  wessf1ornlem  38812  limsupre2lem  39328  icccncfext  39372  stoweidlem14  39506  stoweidlem34  39526  stoweidlem59  39551  etransclem24  39750  nnfoctbdjlem  39947  nnfoctbdj  39948  hspmbllem2  40116  smfmbfcex  40243  nsssmfmbflem  40261  eu2ndop1stv  40474  afvfv0bi  40504  afvco2  40528  ndmaovg  40536  otiunsndisjX  40564  fun2dmnopgexmpl  40569  ltnltne  40579  fmtnoinf  40716  odz2prm2pw  40743  prmdvdsfmtnof1lem2  40765  lighneallem3  40792  lighneallem4  40795  isodd3  40833  bits0ALTV  40858  lidldomnnring  41172  zrninitoringc  41313  ztprmneprm  41367  lindepsnlininds  41484  islindeps  41485  lindslinindsimp2lem5  41494  lindslinindsimp2  41495  difmodm1lt  41560  elsetrecslem  41692
  Copyright terms: Public domain W3C validator