Theorem notbid 633

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 157	. . 3 ⊢ (𝜑 → (𝜒 → 𝜓))
3	2	con3d 601	. 2 ⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜒))
4	1	biimpd 143	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
5	4	con3d 601	. 2 ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓))
6	3, 5	impbid 128	1 ⊢ (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒))

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 584  ax-in2 585

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  notbii  635  stbid  783  dcbid  792  con1biidc  815  pm4.54dc  849  xorbi2d  1326  xorbi1d  1327  pm5.18im  1331  pm5.24dc  1344  neeq1  2280  neeq2  2281  necon3abid  2306  neleq1  2366  neleq2  2367  cdeqnot  2850  ru  2861  sbcng  2901  sbcnel12g  2970  sbcne12g  2971  difjust  3022  eldif  3030  dfdif3  3133  difeq2  3135  disjne  3363  ifbi  3439  prel12  3645  nalset  3998  pwnss  4023  poeq1  4159  pocl  4163  swopo  4166  sotritrieq  4185  tz7.2  4214  regexmidlem1  4386  regexmid  4388  nordeq  4397  nlimsucg  4419  nndceq0  4469  nnregexmid  4472  poinxp  4546  posng  4549  intirr  4861  poirr2  4867  cnvpom  5017  fndmdif  5457  isopolem  5655  poxp  6059  nnmword  6344  brdifun  6386  swoer  6387  2dom  6629  php5  6681  php5dom  6686  findcard2s  6713  fimax2gtrilemstep  6723  fimax2gtri  6724  fidcenumlemrk  6770  supeq3  6792  supeq123d  6793  supmoti  6795  eqsupti  6798  supubti  6801  supsnti  6807  isotilem  6808  isoti  6809  supisolem  6810  supisoex  6811  cnvinfex  6820  cnvti  6821  eqinfti  6822  infvalti  6824  difinfsn  6900  ismkv  6939  mkvprop  6943  fodjumkvlemres  6944  pitric  7030  addnidpig  7045  ltsonq  7107  elinp  7183  prltlu  7196  prdisj  7201  ltexprlemdisj  7315  ltposr  7459  aptisr  7474  axpre-ltirr  7567  axpre-apti  7570  xrlenlt  7701  axapti  7707  lttri3  7715  ltne  7720  leadd1  8059  reapti  8207  lemul1  8221  apirr  8233  apti  8250  apcon4bid  8252  lediv1  8485  lemuldiv  8497  lerec  8500  le2msq  8517  suprnubex  8569  suprleubex  8570  avgle1  8812  avgle2  8813  znnnlt1  8954  supinfneg  9240  infsupneg  9241  eluzdc  9254  qapne  9281  xrltne  9437  xleneg  9461  nn0disj  9756  elfzonelfzo  9848  fvinim0ffz  9859  ioo0  9878  ico0  9880  ioc0  9881  flqlt  9897  expeq0  10165  leisorel  10421  maxleim  10817  maxabslemval  10820  maxleast  10825  minmax  10840  xrmaxleim  10852  xrmaxiflemval  10858  xrmaxlesup  10867  xrminmax  10873  summodclem3  10988  zeo3  11360  odd2np1  11365  mod2eq1n2dvds  11371  ndvdsadd  11423  fldivndvdslt  11427  zsupcllemstep  11433  zsupcllemex  11434  gcdneg  11465  algcvgblem  11523  lcmneg  11548  isprm3  11592  dvdsnprmd  11599  rpexp  11624  pw2dvdslemn  11635  pw2dvdseu  11638  oddpwdclemxy  11639  oddpwdclemdc  11643  oddpwdc  11644  sqpweven  11645  2sqpwodd  11646  sqne2sq  11647  phiprmpw  11690  oddennn  11697  ctinfomlemom  11732  ctinfom  11733  bdxmet  12429  decidi  12583  uzdcinzz  12586  bj-nalset  12674  bj-nnelirr  12736  nninfsellemeq  12794