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  853  drex1  1754  elrnmpt1  4760  xpopth  6042  sbcopeq1a  6053  ltnnnq  7199  ltaddsub  8166  leaddsub  8168  posdif  8185  lesub1  8186  ltsub1  8188  lesub0  8209  possumd  8298  subap0  8372  ltdivmul  8598  ledivmul  8599  zlem1lt  9068  zltlem1  9069  negelrp  9430  fzrev2  9820  fz1sbc  9831  elfzp1b  9832  qtri3or  9975  sumsqeq0  10326  sqrtle  10763  sqrtlt  10764  absgt0ap  10826  iser3shft  11070  dvdssubr  11451  gcdn0gt0  11578  divgcdcoprmex  11695  lmbrf  12295
  Copyright terms: Public domain W3C validator