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  4944  fndmdif  5645  weniso  5868  sbcopeq1a  6188  cfss  7907  posdif  9283  lesub1  9284  lesub0  9306  ltdivmul  9644  ledivmul  9645  ledivmulOLD  9646  zlem1lt  10085  zltlem1  10086  ioon0  10698  fzn  10826  fzrev2  10863  fz1sbc  10875  sumsqeq0  11198  fz1isolem  11415  sqrle  11762  absgt0  11824  isershft  12153  incexc2  12313  dvdssubr  12586  gcdn0gt0  12717  pcfac  12963  ramval  13071  iunocv  16597  lmbrf  17006  perfcls  17109  ovolscalem1  18888  itg2mulclem  19117  sineq0  19905  efif1olem4  19923  atanord  20239  rlimcnp2  20277  bposlem7  20545  rpvmasum2  20677  hial2eq2  21702  adjsym  22429  cnvadj  22488  eigvalcl  22557  mddmd  22897  mdslmd2i  22926  elat2  22936  ballotlemrv  23094  xdivpnfrp  23133  unitdivcld  23300  indpreima  23623  iooscon  23793  elfzp1b  24027  pdivsq  24173  areacirclem2  25028  diophun  26956  jm2.19lem4  27188  isat3  30119  ishlat3N  30166  cvrval5  30226  llnexchb2  30680  lhpoc2N  30826  lhprelat3N  30851  lautcnvle  30900  lautcvr  30903  ltrncnvatb  30949  cdlemb3  31417  cdlemg17h  31479  dih0vbN  32094  djhcvat42  32227  dvh4dimat  32250  mapdordlem2  32449
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