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  1938  elrnmpt1  5088  fndmdif  5807  weniso  6045  sbcopeq1a  6626  cantnffvalOLD  7871  cfss  8434  posdif  9832  lesub1  9833  lesub0  9856  ltdivmul  10204  ledivmul  10205  ledivmulOLD  10206  zlem1lt  10696  zltlem1  10697  ioon0  11326  fzn  11466  fzrev2  11520  fz1sbc  11536  elfzp1b  11537  sumsqeq0  11944  hashfzdm  12202  hashfirdm  12204  fz1isolem  12214  swrdn0  12324  sqrle  12750  absgt0  12812  isershft  13141  incexc2  13301  dvdssubr  13574  gcdn0gt0  13706  pcfac  13961  ramval  14069  ltbwe  17554  iunocv  18106  lmbrf  18864  perfcls  18969  ovolscalem1  20996  itg2mulclem  21224  sineq0  21983  efif1olem4  22001  atanord  22322  rlimcnp2  22360  bposlem7  22629  rpvmasum2  22761  trgcgrg  22967  ebtwntg  23228  hial2eq2  24509  adjsym  25237  cnvadj  25296  eigvalcl  25365  mddmd  25705  mdslmd2i  25734  elat2  25744  negelrp  26037  xdivpnfrp  26108  isorng  26267  unitdivcld  26331  indpreima  26481  iooscon  27136  possumd  27396  pdivsq  27555  areacirclem1  28484  diophun  29112  jm2.19lem4  29341  wwlkm1edg  30367  usg2spthonot0  30408  lincfsuppcl  30947  isat3  32952  ishlat3N  32999  cvrval5  33059  llnexchb2  33513  lhpoc2N  33659  lhprelat3N  33684  lautcnvle  33733  lautcvr  33736  ltrncnvatb  33782  cdlemb3  34250  cdlemg17h  34312  dih0vbN  34927  djhcvat42  35060  dvh4dimat  35083  mapdordlem2  35282