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

Theorem notbid 641
Description: Equivalence property for negation. Deduction form. (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 . 2 (𝜑 → (𝜓𝜒))
2 notbi 640 . 2 ((𝜓𝜒) → (¬ 𝜓 ↔ ¬ 𝜒))
31, 2syl 14 1 (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 588  ax-in2 589
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  stbid  802  dcbid  808  con1biidc  847  pm4.54dc  872  xorbi2d  1343  xorbi1d  1344  pm5.18im  1348  pm5.24dc  1361  neeq1  2298  neeq2  2299  necon3abid  2324  neleq1  2384  neleq2  2385  cdeqnot  2870  ru  2881  sbcng  2921  sbcnel12g  2990  sbcne12g  2991  difjust  3042  eldif  3050  dfdif3  3156  difeq2  3158  disjne  3386  prel12  3668  nalset  4028  pwnss  4053  poeq1  4191  pocl  4195  swopo  4198  sotritrieq  4217  tz7.2  4246  regexmidlem1  4418  regexmid  4420  nordeq  4429  nlimsucg  4451  nndceq0  4501  nnregexmid  4504  poinxp  4578  posng  4581  intirr  4895  poirr2  4901  cnvpom  5051  fndmdif  5493  isopolem  5691  poxp  6097  nnmword  6382  brdifun  6424  swoer  6425  2dom  6667  php5  6720  php5dom  6725  findcard2s  6752  fimax2gtrilemstep  6762  fimax2gtri  6763  fidcenumlemrk  6810  supeq3  6845  supeq123d  6846  supmoti  6848  eqsupti  6851  supubti  6854  supsnti  6860  isotilem  6861  isoti  6862  supisolem  6863  supisoex  6864  cnvinfex  6873  cnvti  6874  eqinfti  6875  infvalti  6877  difinfsn  6953  ismkv  6995  ismkvnex  6997  mkvprop  7000  fodjumkvlemres  7001  pitric  7097  addnidpig  7112  ltsonq  7174  elinp  7250  prltlu  7263  prdisj  7268  ltexprlemdisj  7382  suplocexpr  7501  ltposr  7539  aptisr  7555  suplocsrlem  7584  axpre-ltirr  7658  axpre-apti  7661  axpre-suploclemres  7677  axpre-suploc  7678  xrlenlt  7797  axapti  7803  axsuploc  7805  lttri3  7812  ltne  7817  leadd1  8160  reapti  8309  lemul1  8323  apirr  8335  apti  8352  apcon4bid  8354  lediv1  8595  lemuldiv  8607  lerec  8610  le2msq  8627  suprnubex  8679  suprleubex  8680  avgle1  8928  avgle2  8929  znnnlt1  9070  supinfneg  9358  infsupneg  9359  eluzdc  9372  qapne  9399  xrltne  9564  xleneg  9588  nn0disj  9883  elfzonelfzo  9975  fvinim0ffz  9986  ioo0  10005  ico0  10007  ioc0  10008  flqlt  10024  expeq0  10292  leisorel  10548  maxleim  10945  maxabslemval  10948  maxleast  10953  minmax  10969  xrmaxleim  10981  xrmaxiflemval  10987  xrmaxlesup  10996  xrminmax  11002  summodclem3  11117  zeo3  11492  odd2np1  11497  mod2eq1n2dvds  11503  ndvdsadd  11555  fldivndvdslt  11559  zsupcllemstep  11565  zsupcllemex  11566  gcdneg  11597  algcvgblem  11657  lcmneg  11682  isprm3  11726  dvdsnprmd  11733  rpexp  11758  pw2dvdslemn  11770  pw2dvdseu  11773  oddpwdclemxy  11774  oddpwdclemdc  11778  oddpwdc  11779  sqpweven  11780  2sqpwodd  11781  sqne2sq  11782  phiprmpw  11825  oddennn  11832  ctinfomlemom  11867  ctinfom  11868  bdxmet  12597  dedekindeulemlu  12695  suplociccex  12699  dedekindicclemlu  12704  decidi  12929  uzdcinzz  12932  bj-nalset  13020  bj-nnelirr  13078  subctctexmid  13123  nninfsellemeq  13137
  Copyright terms: Public domain W3C validator