ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  notbid Unicode 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  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
notbid  |-  ( ph  ->  ( -.  ps  <->  -.  ch )
)

Proof of Theorem notbid
StepHypRef Expression
1 notbid.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
2 notbi 655 . 2  |-  ( ( ps  <->  ch )  ->  ( -.  ps  <->  -.  ch )
)
31, 2syl 14 1  |-  ( ph  ->  ( -.  ps  <->  -.  ch )
)
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  7136  addnidpig  7151  ltsonq  7213  elinp  7289  prltlu  7302  prdisj  7307  ltexprlemdisj  7421  suplocexpr  7540  ltposr  7578  aptisr  7594  suplocsrlem  7623  axpre-ltirr  7697  axpre-apti  7700  axpre-suploclemres  7716  axpre-suploc  7717  xrlenlt  7836  axapti  7842  axsuploc  7844  lttri3  7851  ltne  7856  leadd1  8199  reapti  8348  lemul1  8362  apirr  8374  apti  8391  apcon4bid  8393  lediv1  8634  lemuldiv  8646  lerec  8649  le2msq  8666  suprnubex  8718  suprleubex  8719  avgle1  8967  avgle2  8968  znnnlt1  9109  supinfneg  9397  infsupneg  9398  eluzdc  9411  qapne  9438  xrltne  9603  xleneg  9627  nn0disj  9922  elfzonelfzo  10014  fvinim0ffz  10025  ioo0  10044  ico0  10046  ioc0  10047  flqlt  10063  expeq0  10331  leisorel  10587  maxleim  10984  maxabslemval  10987  maxleast  10992  minmax  11008  xrmaxleim  11020  xrmaxiflemval  11026  xrmaxlesup  11035  xrminmax  11041  summodclem3  11156  zeo3  11572  odd2np1  11577  mod2eq1n2dvds  11583  ndvdsadd  11635  fldivndvdslt  11639  zsupcllemstep  11645  zsupcllemex  11646  gcdneg  11677  algcvgblem  11737  lcmneg  11762  isprm3  11806  dvdsnprmd  11813  rpexp  11838  pw2dvdslemn  11850  pw2dvdseu  11853  oddpwdclemxy  11854  oddpwdclemdc  11858  oddpwdc  11859  sqpweven  11860  2sqpwodd  11861  sqne2sq  11862  phiprmpw  11905  oddennn  11912  ctinfomlemom  11947  ctinfom  11948  bdxmet  12680  dedekindeulemlu  12778  suplociccex  12782  dedekindicclemlu  12787  decidi  13016  uzdcinzz  13019  bj-nalset  13107  bj-nnelirr  13165  subctctexmid  13210  nninfsellemeq  13224
  Copyright terms: Public domain W3C validator