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

Theorem bitr2d 189
Description: Deduction form of bitr2i 185. (Contributed by NM, 9-Jun-2004.)
Hypotheses
Ref Expression
bitr2d.1  |-  ( ph  ->  ( ps  <->  ch )
)
bitr2d.2  |-  ( ph  ->  ( ch  <->  th )
)
Assertion
Ref Expression
bitr2d  |-  ( ph  ->  ( th  <->  ps )
)

Proof of Theorem bitr2d
StepHypRef Expression
1 bitr2d.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
2 bitr2d.2 . . 3  |-  ( ph  ->  ( ch  <->  th )
)
31, 2bitrd 188 . 2  |-  ( ph  ->  ( ps  <->  th )
)
43bicomd 141 1  |-  ( ph  ->  ( th  <->  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  3bitrrd  215  3bitr2rd  217  pm5.18dc  884  drex1  1809  elrnmpt1  4896  xpopth  6202  sbcopeq1a  6213  ltnnnq  7453  ltaddsub  8424  leaddsub  8426  posdif  8443  lesub1  8444  ltsub1  8446  lesub0  8467  possumd  8557  subap0  8631  ltdivmul  8864  ledivmul  8865  zlem1lt  9340  zltlem1  9341  negelrp  9719  fzrev2  10117  fz1sbc  10128  elfzp1b  10129  qtri3or  10275  sumsqeq0  10633  sqrtle  11080  sqrtlt  11081  absgt0ap  11143  iser3shft  11389  dvdssubr  11881  gcdn0gt0  12014  divgcdcoprmex  12137  pcfac  12385  lmbrf  14192  logge0b  14788  loggt0b  14789  logle1b  14790  loglt1b  14791  lgsne0  14917  lgsprme0  14921
  Copyright terms: Public domain W3C validator