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

Theorem bitr2d 187
Description: Deduction form of bitr2i 183. (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 186 . 2  |-  ( ph  ->  ( ps  <->  th )
)
43bicomd 139 1  |-  ( ph  ->  ( th  <->  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  3bitrrd  213  3bitr2rd  215  pm5.18dc  811  drex1  1720  elrnmpt1  4613  xpopth  5833  sbcopeq1a  5844  ltnnnq  6675  ltaddsub  7607  leaddsub  7609  posdif  7626  lesub1  7627  ltsub1  7629  lesub0  7650  possumd  7736  ltdivmul  8021  ledivmul  8022  zlem1lt  8488  zltlem1  8489  fzrev2  9178  fz1sbc  9189  elfzp1b  9190  qtri3or  9329  sumsqeq0  9651  sqrtle  10060  sqrtlt  10061  absgt0ap  10123  dvdssubr  10386  gcdn0gt0  10513  divgcdcoprmex  10628
  Copyright terms: Public domain W3C validator