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

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
StepHypRef Expression
1 notbid.1 . . . 4 (𝜑 → (𝜓𝜒))
21biimprd 147 . . 3 (𝜑 → (𝜒𝜓))
32con3d 561 . 2 (𝜑 → (¬ 𝜓 → ¬ 𝜒))
41biimpd 132 . . 3 (𝜑 → (𝜓𝜒))
54con3d 561 . 2 (𝜑 → (¬ 𝜒 → ¬ 𝜓))
63, 5impbid 120 1 (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒))
Colors of variables: wff set class
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  6417  addnidpig  6432  ltsonq  6494  elinp  6570  prltlu  6583  prdisj  6588  ltexprlemdisj  6702  ltposr  6846  aptisr  6861  axpre-ltirr  6954  axpre-apti  6957  xrlenlt  7082  axapti  7088  lttri3  7096  ltne  7101  leadd1  7423  reapti  7568  lemul1  7582  apirr  7594  apti  7611  lediv1  7833  lemuldiv  7845  lerec  7848  le2msq  7865  avgle1  8163  avgle2  8164  znnnlt1  8291  eluzdc  8545  qapne  8572  xrltne  8727  xleneg  8748  nn0disj  8993  elfzonelfzo  9084  fvinim0ffz  9094  flqlt  9123  expeq0  9260  abs00  9636  algcvgblem  9861  bj-nalset  9988  bj-nnelirr  10051
  Copyright terms: Public domain W3C validator