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

Theorem bitr2d 188
Description: Deduction form of bitr2i 184. (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 187 . 2  |-  ( ph  ->  ( ps  <->  th )
)
43bicomd 140 1  |-  ( ph  ->  ( th  <->  ps )
)
Colors of variables: wff set class
Syntax hints:    -> 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
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  3bitrrd  214  3bitr2rd  216  pm5.18dc  851  drex1  1752  elrnmpt1  4758  xpopth  6040  sbcopeq1a  6051  ltnnnq  7195  ltaddsub  8162  leaddsub  8164  posdif  8181  lesub1  8182  ltsub1  8184  lesub0  8205  possumd  8294  subap0  8368  ltdivmul  8594  ledivmul  8595  zlem1lt  9064  zltlem1  9065  negelrp  9426  fzrev2  9816  fz1sbc  9827  elfzp1b  9828  qtri3or  9971  sumsqeq0  10322  sqrtle  10759  sqrtlt  10760  absgt0ap  10822  iser3shft  11066  dvdssubr  11446  gcdn0gt0  11573  divgcdcoprmex  11690  lmbrf  12290
  Copyright terms: Public domain W3C validator