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

Theorem bitr2d 247
Description: Deduction form of bitr2i 243. (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 246 . 2  |-  ( ph  ->  ( ps  <->  th )
)
43bicomd 194 1  |-  ( ph  ->  ( th  <->  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178
This theorem is referenced by:  3bitrrd  273  3bitr2rd  275  pm5.18  347  elrnmpt1  5122  fndmdif  5837  weniso  6078  sbcopeq1a  6402  cfss  8150  posdif  9526  lesub1  9527  lesub0  9549  ltdivmul  9887  ledivmul  9888  ledivmulOLD  9889  zlem1lt  10332  zltlem1  10333  ioon0  10947  fzn  11076  fzrev2  11114  fz1sbc  11129  sumsqeq0  11465  fz1isolem  11715  sqrle  12071  absgt0  12133  isershft  12462  incexc2  12623  dvdssubr  12896  gcdn0gt0  13027  pcfac  13273  ramval  13381  iunocv  16913  lmbrf  17329  perfcls  17434  ovolscalem1  19414  itg2mulclem  19641  sineq0  20434  efif1olem4  20452  atanord  20772  rlimcnp2  20810  bposlem7  21079  rpvmasum2  21211  hial2eq2  22614  adjsym  23341  cnvadj  23400  eigvalcl  23469  mddmd  23809  mdslmd2i  23838  elat2  23848  xdivpnfrp  24184  unitdivcld  24304  indpreima  24427  iooscon  24939  elfzp1b  25121  possumd  25214  pdivsq  25373  areacirclem1  26306  diophun  26846  jm2.19lem4  27077  hashfirdm  28188  hashfzdm  28189  usg2spthonot0  28421  ax7w15lemAUX7  29741  isat3  30179  ishlat3N  30226  cvrval5  30286  llnexchb2  30740  lhpoc2N  30886  lhprelat3N  30911  lautcnvle  30960  lautcvr  30963  ltrncnvatb  31009  cdlemb3  31477  cdlemg17h  31539  dih0vbN  32154  djhcvat42  32287  dvh4dimat  32310  mapdordlem2  32509
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator