MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bitr2d Structured version   Unicode version

Theorem bitr2d 246
Description: Deduction form of bitr2i 242. (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 245 . 2  |-  ( ph  ->  ( ps  <->  th )
)
43bicomd 193 1  |-  ( ph  ->  ( th  <->  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  3bitrrd  272  3bitr2rd  274  pm5.18  346  elrnmpt1  5111  fndmdif  5826  weniso  6067  sbcopeq1a  6391  cfss  8137  posdif  9513  lesub1  9514  lesub0  9536  ltdivmul  9874  ledivmul  9875  ledivmulOLD  9876  zlem1lt  10319  zltlem1  10320  ioon0  10934  fzn  11063  fzrev2  11101  fz1sbc  11116  sumsqeq0  11452  fz1isolem  11702  sqrle  12058  absgt0  12120  isershft  12449  incexc2  12610  dvdssubr  12883  gcdn0gt0  13014  pcfac  13260  ramval  13368  iunocv  16900  lmbrf  17316  perfcls  17421  ovolscalem1  19401  itg2mulclem  19630  sineq0  20421  efif1olem4  20439  atanord  20759  rlimcnp2  20797  bposlem7  21066  rpvmasum2  21198  hial2eq2  22601  adjsym  23328  cnvadj  23387  eigvalcl  23456  mddmd  23796  mdslmd2i  23825  elat2  23835  xdivpnfrp  24171  unitdivcld  24291  indpreima  24414  iooscon  24926  elfzp1b  25108  possumd  25201  pdivsq  25360  areacirclem2  26282  diophun  26823  jm2.19lem4  27054  hashfirdm  28143  hashfzdm  28144  usg2spthonot0  28309  ax7w15lemAUX7  29604  isat3  30042  ishlat3N  30089  cvrval5  30149  llnexchb2  30603  lhpoc2N  30749  lhprelat3N  30774  lautcnvle  30823  lautcvr  30826  ltrncnvatb  30872  cdlemb3  31340  cdlemg17h  31402  dih0vbN  32017  djhcvat42  32150  dvh4dimat  32173  mapdordlem2  32372
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator