ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  notbid GIF version

Theorem notbid 602
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
StepHypRef Expression
1 notbid.1 . . . 4 (𝜑 → (𝜓𝜒))
21biimprd 151 . . 3 (𝜑 → (𝜒𝜓))
32con3d 571 . 2 (𝜑 → (¬ 𝜓 → ¬ 𝜒))
41biimpd 136 . . 3 (𝜑 → (𝜓𝜒))
54con3d 571 . 2 (𝜑 → (¬ 𝜒 → ¬ 𝜓))
63, 5impbid 124 1 (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-in1 554  ax-in2 555
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  notbii  604  dcbid  759  con1biidc  782  pm4.54dc  816  xorbi2d  1287  xorbi1d  1288  pm5.18im  1292  pm5.24dc  1305  neeq1  2233  neeq2  2234  necon3abid  2259  neleq1  2318  neleq2  2319  cdeqnot  2775  ru  2786  sbcng  2826  sbcnel12g  2895  sbcne12g  2896  difjust  2947  eldif  2955  dfpss3  3058  difeq2  3084  disjne  3301  ifbi  3376  prel12  3570  nalset  3915  pwnss  3940  poeq1  4064  pocl  4068  swopo  4071  sotritrieq  4090  tz7.2  4119  regexmidlem1  4286  regexmid  4288  nordeq  4296  nlimsucg  4318  nndceq0  4367  nnregexmid  4370  poinxp  4437  posng  4440  intirr  4739  poirr2  4745  cnvpom  4888  fndmdif  5300  f1imapss  5443  isopolem  5489  poxp  5881  nnmword  6122  brdifun  6164  swoer  6165  2dom  6316  php5  6352  php5dom  6356  findcard2s  6378  supeq3  6396  supeq123d  6397  supmoti  6399  eqsupti  6402  supubti  6405  supsnti  6409  isotilem  6410  isoti  6411  supisolem  6412  supisoex  6413  pitric  6477  addnidpig  6492  ltsonq  6554  elinp  6630  prltlu  6643  prdisj  6648  ltexprlemdisj  6762  ltposr  6906  aptisr  6921  axpre-ltirr  7014  axpre-apti  7017  xrlenlt  7143  axapti  7149  lttri3  7157  ltne  7162  leadd1  7499  reapti  7644  lemul1  7658  apirr  7670  apti  7687  lediv1  7910  lemuldiv  7922  lerec  7925  le2msq  7942  avgle1  8222  avgle2  8223  znnnlt1  8350  eluzdc  8644  qapne  8671  xrltne  8830  xleneg  8851  nn0disj  9097  elfzonelfzo  9188  fvinim0ffz  9198  ioo0  9216  ico0  9218  ioc0  9219  flqlt  9233  expeq0  9451  abs00  9891  zeo3  10179  odd2np1  10184  mod2eq1n2dvds  10191  ndvdsadd  10243  fldivndvdslt  10247  pw2dvdslemn  10253  pw2dvdseu  10256  oddpwdclemxy  10257  oddpwdclemdc  10261  oddpwdc  10262  algcvgblem  10271  bj-nalset  10402  bj-nnelirr  10465
  Copyright terms: Public domain W3C validator