Theorem notbid 592

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 147	. . 3 ⊢ (𝜑 → (𝜒 → 𝜓))
3	2	con3d 561	. 2 ⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜒))
4	1	biimpd 132	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
5	4	con3d 561	. 2 ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓))
6	3, 5	impbid 120	1 ⊢ (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒))

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  notbii  594  dcbid  748  con1biidc  771  pm4.54dc  805  xorbi2d  1271  xorbi1d  1272  pm5.18im  1276  pm5.24dc  1289  neeq1  2218  neeq2  2219  necon3abid  2244  neleq1  2301  neleq2  2302  cdeqnot  2752  ru  2763  sbcng  2803  sbcnel12g  2867  sbcne12g  2868  difjust  2919  eldif  2927  dfpss3  3030  difeq2  3056  disjne  3273  ifbi  3348  prel12  3542  nalset  3887  pwnss  3912  poeq1  4036  pocl  4040  swopo  4043  sotritrieq  4062  tz7.2  4091  regexmidlem1  4258  regexmid  4260  nordeq  4268  nlimsucg  4290  nndceq0  4339  nnregexmid  4342  poinxp  4409  posng  4412  intirr  4711  poirr2  4717  cnvpom  4860  fndmdif  5272  f1imapss  5415  isopolem  5461  poxp  5853  nnmword  6091  brdifun  6133  swoer  6134  2dom  6285  php5  6321  php5dom  6325  findcard2s  6347  pitric  6419  addnidpig  6434  ltsonq  6496  elinp  6572  prltlu  6585  prdisj  6590  ltexprlemdisj  6704  ltposr  6848  aptisr  6863  axpre-ltirr  6956  axpre-apti  6959  xrlenlt  7084  axapti  7090  lttri3  7098  ltne  7103  leadd1  7425  reapti  7570  lemul1  7584  apirr  7596  apti  7613  lediv1  7835  lemuldiv  7847  lerec  7850  le2msq  7867  avgle1  8165  avgle2  8166  znnnlt1  8293  eluzdc  8547  qapne  8574  xrltne  8729  xleneg  8750  nn0disj  8995  elfzonelfzo  9086  fvinim0ffz  9096  flqlt  9125  expeq0  9286  abs00  9662  algcvgblem  9888  bj-nalset  10015  bj-nnelirr  10078