Theorem notbid 625

Description: Deduction negating both sides of a logical equivalence. (Contributed by NM, 21-May-1994.) (Revised by Mario Carneiro, 31-Jan-2015.)

Hypothesis

Ref	Expression
notbid.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
notbid	⊢ (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒))

Proof of Theorem notbid

Step	Hyp	Ref	Expression
1		notbid.1	. . . 4 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	biimprd 156	. . 3 ⊢ (𝜑 → (𝜒 → 𝜓))
3	2	con3d 594	. 2 ⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜒))
4	1	biimpd 142	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
5	4	con3d 594	. 2 ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓))
6	3, 5	impbid 127	1 ⊢ (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  notbii  627  stbid  775  dcbid  784  con1biidc  807  pm4.54dc  841  xorbi2d  1314  xorbi1d  1315  pm5.18im  1319  pm5.24dc  1332  neeq1  2264  neeq2  2265  necon3abid  2290  neleq1  2350  neleq2  2351  cdeqnot  2817  ru  2828  sbcng  2868  sbcnel12g  2937  sbcne12g  2938  difjust  2989  eldif  2997  dfdif3  3099  difeq2  3101  disjne  3324  ifbi  3397  prel12  3600  nalset  3946  pwnss  3971  poeq1  4102  pocl  4106  swopo  4109  sotritrieq  4128  tz7.2  4157  regexmidlem1  4324  regexmid  4326  nordeq  4335  nlimsucg  4357  nndceq0  4406  nnregexmid  4409  poinxp  4477  posng  4480  intirr  4787  poirr2  4793  cnvpom  4941  fndmdif  5369  isopolem  5564  poxp  5956  nnmword  6231  brdifun  6273  swoer  6274  2dom  6476  php5  6528  php5dom  6533  findcard2s  6560  fimax2gtrilemstep  6570  fimax2gtri  6571  supeq3  6632  supeq123d  6633  supmoti  6635  eqsupti  6638  supubti  6641  supsnti  6647  isotilem  6648  isoti  6649  supisolem  6650  supisoex  6651  cnvinfex  6660  cnvti  6661  eqinfti  6662  infvalti  6664  pitric  6827  addnidpig  6842  ltsonq  6904  elinp  6980  prltlu  6993  prdisj  6998  ltexprlemdisj  7112  ltposr  7256  aptisr  7271  axpre-ltirr  7364  axpre-apti  7367  xrlenlt  7498  axapti  7504  lttri3  7512  ltne  7517  leadd1  7855  reapti  8000  lemul1  8014  apirr  8026  apti  8043  lediv1  8268  lemuldiv  8280  lerec  8283  le2msq  8300  suprnubex  8352  suprleubex  8353  avgle1  8592  avgle2  8593  znnnlt1  8734  supinfneg  9018  infsupneg  9019  eluzdc  9032  qapne  9059  xrltne  9213  xleneg  9234  nn0disj  9480  elfzonelfzo  9572  fvinim0ffz  9583  ioo0  9602  ico0  9604  ioc0  9605  flqlt  9621  expeq0  9888  leisorel  10142  abs00  10396  maxleim  10537  maxabslemval  10540  maxleast  10545  minmax  10559  isummolem3  10664  zeo3  10774  odd2np1  10779  mod2eq1n2dvds  10785  ndvdsadd  10837  fldivndvdslt  10841  zsupcllemstep  10847  zsupcllemex  10848  gcdneg  10879  algcvgblem  10937  lcmneg  10962  isprm3  11006  dvdsnprmd  11013  rpexp  11038  pw2dvdslemn  11049  pw2dvdseu  11052  oddpwdclemxy  11053  oddpwdclemdc  11057  oddpwdc  11058  sqpweven  11059  2sqpwodd  11060  sqne2sq  11061  phiprmpw  11104  oddennn  11111  decidi  11164  uzdcinzz  11167  bj-nalset  11255  bj-nnelirr  11317  nninfsellemeq  11375