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

Theorem notbid 656
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 655 . 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 603  ax-in2 604
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  stbid  817  dcbid  823  con1biidc  862  pm4.54dc  887  xorbi2d  1358  xorbi1d  1359  pm5.18im  1363  pm5.24dc  1376  neeq1  2321  neeq2  2322  necon3abid  2347  neleq1  2407  neleq2  2408  cdeqnot  2897  ru  2908  sbcng  2949  sbcnel12g  3019  sbcne12g  3020  difjust  3072  eldif  3080  dfdif3  3186  difeq2  3188  disjne  3416  prel12  3698  nalset  4058  pwnss  4083  poeq1  4221  pocl  4225  swopo  4228  sotritrieq  4247  tz7.2  4276  regexmidlem1  4448  regexmid  4450  nordeq  4459  nlimsucg  4481  nndceq0  4531  nnregexmid  4534  poinxp  4608  posng  4611  intirr  4925  poirr2  4931  cnvpom  5081  fndmdif  5525  isopolem  5723  poxp  6129  nnmword  6414  brdifun  6456  swoer  6457  2dom  6699  php5  6752  php5dom  6757  findcard2s  6784  fimax2gtrilemstep  6794  fimax2gtri  6795  fidcenumlemrk  6842  supeq3  6877  supeq123d  6878  supmoti  6880  eqsupti  6883  supubti  6886  supsnti  6892  isotilem  6893  isoti  6894  supisolem  6895  supisoex  6896  cnvinfex  6905  cnvti  6906  eqinfti  6907  infvalti  6909  difinfsn  6985  ismkv  7027  ismkvnex  7029  mkvprop  7032  fodjumkvlemres  7033  pitric  7141  addnidpig  7156  ltsonq  7218  elinp  7294  prltlu  7307  prdisj  7312  ltexprlemdisj  7426  suplocexpr  7545  ltposr  7583  aptisr  7599  suplocsrlem  7628  axpre-ltirr  7702  axpre-apti  7705  axpre-suploclemres  7721  axpre-suploc  7722  xrlenlt  7841  axapti  7847  axsuploc  7849  lttri3  7856  ltne  7861  leadd1  8204  reapti  8353  lemul1  8367  apirr  8379  apti  8396  apcon4bid  8398  lediv1  8639  lemuldiv  8651  lerec  8654  le2msq  8671  suprnubex  8723  suprleubex  8724  avgle1  8972  avgle2  8973  znnnlt1  9114  supinfneg  9402  infsupneg  9403  eluzdc  9416  qapne  9443  xrltne  9608  xleneg  9632  nn0disj  9927  elfzonelfzo  10019  fvinim0ffz  10030  ioo0  10049  ico0  10051  ioc0  10052  flqlt  10068  expeq0  10336  leisorel  10592  maxleim  10989  maxabslemval  10992  maxleast  10997  minmax  11013  xrmaxleim  11025  xrmaxiflemval  11031  xrmaxlesup  11040  xrminmax  11046  summodclem3  11161  zeo3  11576  odd2np1  11581  mod2eq1n2dvds  11587  ndvdsadd  11639  fldivndvdslt  11643  zsupcllemstep  11649  zsupcllemex  11650  gcdneg  11681  algcvgblem  11741  lcmneg  11766  isprm3  11810  dvdsnprmd  11817  rpexp  11842  pw2dvdslemn  11854  pw2dvdseu  11857  oddpwdclemxy  11858  oddpwdclemdc  11862  oddpwdc  11863  sqpweven  11864  2sqpwodd  11865  sqne2sq  11866  phiprmpw  11909  oddennn  11916  ctinfomlemom  11951  ctinfom  11952  bdxmet  12684  dedekindeulemlu  12782  suplociccex  12786  dedekindicclemlu  12791  efle  12880  logleb  12976  decidi  13061  uzdcinzz  13064  bj-nalset  13152  bj-nnelirr  13210  subctctexmid  13255  nninfsellemeq  13271
  Copyright terms: Public domain W3C validator