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

Theorem notbid 602
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  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
notbid  |-  ( ph  ->  ( -.  ps  <->  -.  ch )
)

Proof of Theorem notbid
StepHypRef Expression
1 notbid.1 . . . 4  |-  ( ph  ->  ( ps  <->  ch )
)
21biimprd 151 . . 3  |-  ( ph  ->  ( ch  ->  ps ) )
32con3d 571 . 2  |-  ( ph  ->  ( -.  ps  ->  -. 
ch ) )
41biimpd 136 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
54con3d 571 . 2  |-  ( ph  ->  ( -.  ch  ->  -. 
ps ) )
63, 5impbid 124 1  |-  ( ph  ->  ( -.  ps  <->  -.  ch )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-in1 554  ax-in2 555
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  notbii  604  dcbid  759  con1biidc  782  pm4.54dc  816  xorbi2d  1287  xorbi1d  1288  pm5.18im  1292  pm5.24dc  1305  neeq1  2233  neeq2  2234  necon3abid  2259  neleq1  2318  neleq2  2319  cdeqnot  2774  ru  2785  sbcng  2825  sbcnel12g  2894  sbcne12g  2895  difjust  2946  eldif  2954  dfpss3  3057  difeq2  3083  disjne  3300  ifbi  3375  prel12  3569  nalset  3914  pwnss  3939  poeq1  4063  pocl  4067  swopo  4070  sotritrieq  4089  tz7.2  4118  regexmidlem1  4285  regexmid  4287  nordeq  4295  nlimsucg  4317  nndceq0  4366  nnregexmid  4369  poinxp  4436  posng  4439  intirr  4738  poirr2  4744  cnvpom  4887  fndmdif  5299  f1imapss  5442  isopolem  5488  poxp  5880  nnmword  6121  brdifun  6163  swoer  6164  2dom  6315  php5  6351  php5dom  6355  findcard2s  6377  supeq3  6395  supeq123d  6396  supmoti  6398  eqsupti  6401  supubti  6404  supsnti  6408  isotilem  6409  isoti  6410  supisolem  6411  supisoex  6412  pitric  6476  addnidpig  6491  ltsonq  6553  elinp  6629  prltlu  6642  prdisj  6647  ltexprlemdisj  6761  ltposr  6905  aptisr  6920  axpre-ltirr  7013  axpre-apti  7016  xrlenlt  7142  axapti  7148  lttri3  7156  ltne  7161  leadd1  7498  reapti  7643  lemul1  7657  apirr  7669  apti  7686  lediv1  7909  lemuldiv  7921  lerec  7924  le2msq  7941  avgle1  8221  avgle2  8222  znnnlt1  8349  eluzdc  8643  qapne  8670  xrltne  8829  xleneg  8850  nn0disj  9096  elfzonelfzo  9187  fvinim0ffz  9197  ioo0  9215  ico0  9217  ioc0  9218  flqlt  9232  expeq0  9450  abs00  9890  zeo3  10178  odd2np1  10183  mod2eq1n2dvds  10190  pw2dvdslemn  10239  pw2dvdseu  10242  oddpwdclemxy  10243  oddpwdclemdc  10247  oddpwdc  10248  algcvgblem  10257  bj-nalset  10388  bj-nnelirr  10451
  Copyright terms: Public domain W3C validator