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

Theorem notbid 630
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 157 . . 3  |-  ( ph  ->  ( ch  ->  ps ) )
32con3d 599 . 2  |-  ( ph  ->  ( -.  ps  ->  -. 
ch ) )
41biimpd 143 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
54con3d 599 . 2  |-  ( ph  ->  ( -.  ch  ->  -. 
ps ) )
63, 5impbid 128 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-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 582  ax-in2 583
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  notbii  632  stbid  780  dcbid  789  con1biidc  812  pm4.54dc  846  xorbi2d  1323  xorbi1d  1324  pm5.18im  1328  pm5.24dc  1341  neeq1  2275  neeq2  2276  necon3abid  2301  neleq1  2361  neleq2  2362  cdeqnot  2842  ru  2853  sbcng  2893  sbcnel12g  2962  sbcne12g  2963  difjust  3014  eldif  3022  dfdif3  3125  difeq2  3127  disjne  3355  ifbi  3431  prel12  3637  nalset  3990  pwnss  4015  poeq1  4150  pocl  4154  swopo  4157  sotritrieq  4176  tz7.2  4205  regexmidlem1  4377  regexmid  4379  nordeq  4388  nlimsucg  4410  nndceq0  4459  nnregexmid  4462  poinxp  4536  posng  4539  intirr  4851  poirr2  4857  cnvpom  5007  fndmdif  5443  isopolem  5639  poxp  6035  nnmword  6317  brdifun  6359  swoer  6360  2dom  6602  php5  6654  php5dom  6659  findcard2s  6686  fimax2gtrilemstep  6696  fimax2gtri  6697  fidcenumlemrk  6743  supeq3  6765  supeq123d  6766  supmoti  6768  eqsupti  6771  supubti  6774  supsnti  6780  isotilem  6781  isoti  6782  supisolem  6783  supisoex  6784  cnvinfex  6793  cnvti  6794  eqinfti  6795  infvalti  6797  ismkv  6897  mkvprop  6901  fodjumkvlemres  6902  pitric  6977  addnidpig  6992  ltsonq  7054  elinp  7130  prltlu  7143  prdisj  7148  ltexprlemdisj  7262  ltposr  7406  aptisr  7421  axpre-ltirr  7514  axpre-apti  7517  xrlenlt  7648  axapti  7654  lttri3  7662  ltne  7667  leadd1  8005  reapti  8153  lemul1  8167  apirr  8179  apti  8196  lediv1  8427  lemuldiv  8439  lerec  8442  le2msq  8459  suprnubex  8511  suprleubex  8512  avgle1  8754  avgle2  8755  znnnlt1  8896  supinfneg  9182  infsupneg  9183  eluzdc  9196  qapne  9223  xrltne  9379  xleneg  9403  nn0disj  9698  elfzonelfzo  9790  fvinim0ffz  9801  ioo0  9820  ico0  9822  ioc0  9823  flqlt  9839  expeq0  10117  leisorel  10373  abs00  10628  maxleim  10769  maxabslemval  10772  maxleast  10777  minmax  10792  xrmaxleim  10803  xrmaxiflemval  10809  xrmaxlesup  10818  xrminmax  10824  summodclem3  10939  zeo3  11311  odd2np1  11316  mod2eq1n2dvds  11322  ndvdsadd  11374  fldivndvdslt  11378  zsupcllemstep  11384  zsupcllemex  11385  gcdneg  11416  algcvgblem  11474  lcmneg  11499  isprm3  11543  dvdsnprmd  11550  rpexp  11575  pw2dvdslemn  11586  pw2dvdseu  11589  oddpwdclemxy  11590  oddpwdclemdc  11594  oddpwdc  11595  sqpweven  11596  2sqpwodd  11597  sqne2sq  11598  phiprmpw  11641  oddennn  11648  bdxmet  12303  decidi  12419  uzdcinzz  12422  bj-nalset  12510  bj-nnelirr  12572  nninfsellemeq  12627
  Copyright terms: Public domain W3C validator