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  356  sbequ12a  1963  elrnmpt1  5257  fndmdif  5992  weniso  6249  sbcopeq1a  6847  cantnffvalOLD  8094  cfss  8657  posdif  10057  lesub1  10058  lesub0  10081  ltdivmul  10429  ledivmul  10430  ledivmulOLD  10431  zlem1lt  10926  zltlem1  10927  ioon0  11567  fzn  11714  fzrev2  11755  fz1sbc  11766  elfzp1b  11767  sumsqeq0  12226  hashfzdm  12479  hashfirdm  12481  fz1isolem  12491  swrdn0  12635  sqrtle  13074  absgt0  13137  isershft  13466  incexc2  13630  dvdssubr  13903  gcdn0gt0  14036  pcfac  14294  ramval  14402  ltbwe  18007  iunocv  18581  lmbrf  19629  perfcls  19734  ovolscalem1  21792  itg2mulclem  22021  sineq0  22780  efif1olem4  22798  atanord  23124  rlimcnp2  23162  bposlem7  23431  rpvmasum2  23563  trgcgrg  23772  legov3  23849  ebtwntg  24108  wwlkm1edg  24558  usg2spthonot0  24712  hial2eq2  25847  adjsym  26575  cnvadj  26634  eigvalcl  26703  mddmd  27043  mdslmd2i  27072  elat2  27082  negelrp  27387  xdivpnfrp  27453  isorng  27614  unitdivcld  27708  indpreima  27863  iooscon  28517  possumd  28942  pdivsq  29101  areacirclem1  30034  diophun  30635  jm2.19lem4  30862  lincfsuppcl  32496  isat3  34505  ishlat3N  34552  cvrval5  34612  llnexchb2  35066  lhpoc2N  35212  lhprelat3N  35237  lautcnvle  35286  lautcvr  35289  ltrncnvatb  35335  cdlemb3  35803  cdlemg17h  35865  dih0vbN  36480  djhcvat42  36613  dvh4dimat  36636  mapdordlem2  36835