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  2216  neeq2  2217  necon3abid  2241  neleq1  2298  neleq2  2299  cdeqnot  2749  ru  2760  sbcng  2800  sbcnel12g  2864  sbcne12g  2865  difjust  2916  eldif  2924  dfpss3  3027  difeq2  3053  disjne  3270  ifbi  3345  prel12  3539  nalset  3884  pwnss  3909  poeq1  4033  pocl  4037  swopo  4040  sotritrieq  4059  tz7.2  4087  regexmidlem1  4254  regexmid  4255  nordeq  4262  nlimsucg  4284  nndceq0  4326  nnregexmid  4329  poinxp  4396  posng  4399  intirr  4698  poirr2  4704  cnvpom  4847  fndmdif  5259  f1imapss  5402  isopolem  5448  poxp  5840  nnmword  6078  brdifun  6120  swoer  6121  2dom  6272  php5  6308  php5dom  6312  findcard2s  6333  pitric  6400  addnidpig  6415  ltsonq  6477  elinp  6553  prltlu  6566  prdisj  6571  ltexprlemdisj  6685  ltposr  6829  aptisr  6844  axpre-ltirr  6937  axpre-apti  6940  xrlenlt  7064  axapti  7070  lttri3  7078  ltne  7083  leadd1  7403  reapti  7546  lemul1  7560  apirr  7572  apti  7589  lediv1  7811  lemuldiv  7823  lerec  7826  le2msq  7843  avgle1  8138  avgle2  8139  znnnlt1  8265  eluzdc  8519  qapne  8546  xrltne  8696  xleneg  8717  nn0disj  8962  elfzonelfzo  9053  expeq0  9164  abs00  9540  algcvgblem  9765  bj-nalset  9888  bj-nnelirr  9951
  Copyright terms: Public domain W3C validator