Theorem bitr2d 254

Description: Deduction form of bitr2i 250. (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

Step	Hyp	Ref	Expression
1		bitr2d.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2		bitr2d.2	. . 3 |- ( ph -> ( ch <-> th ) )
3	1, 2	bitrd 253	. 2 |- ( ph -> ( ps <-> th ) )
4	3	bicomd 201	1 |- ( ph -> ( th <-> ps ) )

Syntax hints:   -> wi 4   <-> wb 184

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 185

This theorem is referenced by:  3bitrrd  280  3bitr2rd  282  pm5.18  354  sbequ12a  1999  elrnmpt1  5240  fndmdif  5967  weniso  6225  sbcopeq1a  6825  cantnffvalOLD  8073  cfss  8636  posdif  10041  lesub1  10042  lesub0  10065  ltdivmul  10413  ledivmul  10414  zlem1lt  10911  zltlem1  10912  ioon0  11558  fzn  11705  fzrev2  11747  fz1sbc  11758  elfzp1b  11759  sumsqeq0  12231  hashfzdm  12485  hashfirdm  12487  fz1isolem  12497  sqrtle  13179  absgt0  13242  isershft  13571  incexc2  13735  dvdssubr  14114  gcdn0gt0  14247  pcfac  14505  ramval  14613  ltbwe  18335  iunocv  18888  lmbrf  19931  perfcls  20036  ovolscalem1  22093  itg2mulclem  22322  sineq0  23083  efif1olem4  23101  atanord  23458  rlimcnp2  23497  bposlem7  23766  rpvmasum2  23898  trgcgrg  24110  legov3  24188  opphllem6  24328  ebtwntg  24490  wwlkm1edg  24940  usg2spthonot0  25094  hial2eq2  26225  adjsym  26953  cnvadj  27012  eigvalcl  27081  mddmd  27421  mdslmd2i  27450  elat2  27460  negelrp  27798  xdivpnfrp  27866  isorng  28027  unitdivcld  28121  indpreima  28257  iooscon  28959  possumd  29360  pdivsq  29418  areacirclem1  30350  diophun  30949  jm2.19lem4  31176  isrnghm  32971  lincfsuppcl  33287  logge0b  33425  loggt0b  33426  logle1b  33427  loglt1b  33428  isat3  35448  ishlat3N  35495  cvrval5  35555  llnexchb2  36009  lhpoc2N  36155  lhprelat3N  36180  lautcnvle  36229  lautcvr  36232  ltrncnvatb  36278  cdlemb3  36748  cdlemg17h  36810  dih0vbN  37425  djhcvat42  37558  dvh4dimat  37581  mapdordlem2  37780