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

Theorem notbid 579
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 548 . 2 (φ → (¬ ψ → ¬ χ))
41biimpd 132 . . 3 (φ → (ψχ))
54con3d 548 . 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 532  ax-in2 533
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  notbii  581  dcbid  736  con1biidc  759  pm4.54dc  793  xorbi2d  1253  xorbi1d  1254  pm5.18im  1257  pm5.24dc  1270  neeq1  2193  neeq2  2194  necon3abid  2218  neleq1  2275  neleq2  2276  cdeqnot  2725  ru  2736  sbcng  2776  sbcnel12g  2840  sbcne12g  2841  difjust  2892  eldif  2900  dfpss3  3003  difeq2  3029  disjne  3246  ifbi  3321  prel12  3512  nalset  3857  pwnss  3882  poeq1  4006  pocl  4010  swopo  4013  sotritrieq  4032  regexmidlem1  4198  regexmid  4199  nlimsucg  4222  nndceq0  4262  nnregexmid  4265  poinxp  4332  posng  4335  intirr  4634  poirr2  4640  cnvpom  4783  fndmdif  5193  f1imapss  5336  isopolem  5382  poxp  5771  nnmword  5998  brdifun  6040  swoer  6041  pitric  6175  addnidpig  6190  ltsonq  6251  elinp  6322  prltlu  6335  prdisj  6340  ltexprlemdisj  6437  ltposr  6507  aptisr  6521  axpre-ltirr  6575  axpre-apti  6578  xrlenlt  6686  axapti  6692  lttri3  6700  ltne  6705  leadd1  7025  reapti  7168  lemul1  7180  apirr  7189  bj-nalset  7310  bj-nnelirr  7371
  Copyright terms: Public domain W3C validator