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

Theorem notbid 576
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 545 . 2 (φ → (¬ ψ → ¬ χ))
41biimpd 132 . . 3 (φ → (ψχ))
54con3d 545 . 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 529  ax-in2 530
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  notbii  578  dcbid  732  con1biidc  755  pm4.54dc  789  xorbi2d  1253  xorbi1d  1254  pm5.18im  1257  pm5.24dc  1270  neeq1  2191  neeq2  2192  necon3abid  2216  neleq1  2273  neleq2  2274  cdeqnot  2723  ru  2734  sbcng  2774  sbcnel12g  2838  sbcne12g  2839  difjust  2890  eldif  2898  dfpss3  3001  difeq2  3027  disjne  3244  ifbi  3317  prel12  3508  nalset  3853  pwnss  3878  poeq1  4002  pocl  4006  swopo  4009  sotritrieq  4028  regexmidlem1  4193  regexmid  4194  nlimsucg  4217  nndceq0  4257  nnregexmid  4260  poinxp  4327  posng  4330  intirr  4629  poirr2  4635  cnvpom  4778  fndmdif  5188  f1imapss  5331  isopolem  5377  poxp  5766  nnmword  5993  brdifun  6035  swoer  6036  pitric  6170  addnidpig  6185  ltsonq  6246  elinp  6317  prltlu  6330  prdisj  6335  ltexprlemdisj  6432  ltposr  6504  aptisr  6518  axpre-ltirr  6574  axpre-apti  6577  xrlenlt  6687  axapti  6693  lttri3  6701  ltne  6706  leadd1  7026  reapti  7169  lemul1  7183  apirr  7195  apti  7212  lediv1  7421  lemuldiv  7433  lerec  7436  le2msq  7453  avgle1  7746  avgle2  7747  znnnlt1  7867  qapne  8060  xrltne  8208  xleneg  8229  bj-nalset  8468  bj-nnelirr  8529
  Copyright terms: Public domain W3C validator