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

Theorem notbid 591
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 560 . 2 (φ → (¬ ψ → ¬ χ))
41biimpd 132 . . 3 (φ → (ψχ))
54con3d 560 . 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  593  dcbid  747  con1biidc  770  pm4.54dc  804  xorbi2d  1269  xorbi1d  1270  pm5.18im  1273  pm5.24dc  1286  neeq1  2213  neeq2  2214  necon3abid  2238  neleq1  2295  neleq2  2296  cdeqnot  2746  ru  2757  sbcng  2797  sbcnel12g  2861  sbcne12g  2862  difjust  2913  eldif  2921  dfpss3  3024  difeq2  3050  disjne  3267  ifbi  3342  prel12  3533  nalset  3878  pwnss  3903  poeq1  4027  pocl  4031  swopo  4034  sotritrieq  4053  regexmidlem1  4218  regexmid  4219  nlimsucg  4242  nndceq0  4282  nnregexmid  4285  poinxp  4352  posng  4355  intirr  4654  poirr2  4660  cnvpom  4803  fndmdif  5215  f1imapss  5358  isopolem  5404  poxp  5794  nnmword  6027  brdifun  6069  swoer  6070  2dom  6221  pitric  6305  addnidpig  6320  ltsonq  6382  elinp  6456  prltlu  6469  prdisj  6474  ltexprlemdisj  6579  ltposr  6671  aptisr  6685  axpre-ltirr  6746  axpre-apti  6749  xrlenlt  6861  axapti  6867  lttri3  6875  ltne  6880  leadd1  7200  reapti  7343  lemul1  7357  apirr  7369  apti  7386  lediv1  7596  lemuldiv  7608  lerec  7611  le2msq  7628  avgle1  7922  avgle2  7923  znnnlt1  8049  eluzdc  8303  qapne  8330  xrltne  8479  xleneg  8500  nn0disj  8745  elfzonelfzo  8836  expeq0  8920  bj-nalset  9326  bj-nnelirr  9387
  Copyright terms: Public domain W3C validator