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

Theorem bitr2d 245
Description: Deduction form of bitr2i 241. (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 244 . 2  |-  ( ph  ->  ( ps  <->  th )
)
43bicomd 192 1  |-  ( ph  ->  ( th  <->  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  3bitrrd  271  3bitr2rd  273  pm5.18  345  elrnmpt1  4928  fndmdif  5629  weniso  5852  sbcopeq1a  6172  cfss  7891  posdif  9267  lesub1  9268  lesub0  9290  ltdivmul  9628  ledivmul  9629  ledivmulOLD  9630  zlem1lt  10069  zltlem1  10070  ioon0  10682  fzn  10810  fzrev2  10847  fz1sbc  10859  sumsqeq0  11182  fz1isolem  11399  sqrle  11746  absgt0  11808  isershft  12137  incexc2  12297  dvdssubr  12570  gcdn0gt0  12701  pcfac  12947  ramval  13055  iunocv  16581  lmbrf  16990  perfcls  17093  ovolscalem1  18872  itg2mulclem  19101  sineq0  19889  efif1olem4  19907  atanord  20223  rlimcnp2  20261  bposlem7  20529  rpvmasum2  20661  hial2eq2  21686  adjsym  22413  cnvadj  22472  eigvalcl  22541  mddmd  22881  mdslmd2i  22910  elat2  22920  ballotlemrv  23078  xdivpnfrp  23117  unitdivcld  23285  indpreima  23608  iooscon  23778  elfzp1b  24012  pdivsq  24102  areacirclem2  24925  diophun  26853  jm2.19lem4  27085  isat3  29497  ishlat3N  29544  cvrval5  29604  llnexchb2  30058  lhpoc2N  30204  lhprelat3N  30229  lautcnvle  30278  lautcvr  30281  ltrncnvatb  30327  cdlemb3  30795  cdlemg17h  30857  dih0vbN  31472  djhcvat42  31605  dvh4dimat  31628  mapdordlem2  31827
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 177
  Copyright terms: Public domain W3C validator