Theorem bitr2d 269

Description: Deduction form of bitr2i 265. (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 268	. 2 |- ( ph -> ( ps <-> th ) )
4	3	bicomd 213	1 |- ( ph -> ( th <-> ps ) )

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

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 197

This theorem is referenced by:  3bitrrd  295  3bitr2rd  297  pm5.18  371  ifptru  1023  sbequ12a  2113  elrnmpt1  5374  fndmdif  6321  weniso  6604  sbcopeq1a  7220  cfss  9087  posdif  10521  lesub1  10522  lesub0  10545  possumd  10652  ltdivmul  10898  ledivmul  10899  zlem1lt  11429  zltlem1  11430  negelrp  11864  ioon0  12201  fzn  12357  fzrev2  12404  fz1sbc  12416  elfzp1b  12417  sumsqeq0  12942  fz1isolem  13245  sqrtle  14001  absgt0  14064  isershft  14394  incexc2  14570  dvdssubr  15027  gcdn0gt0  15239  divgcdcoprmex  15380  pcfac  15603  ramval  15712  ltbwe  19472  iunocv  20025  lmbrf  21064  perfcls  21169  ovolscalem1  23281  itg2mulclem  23513  sineq0  24273  efif1olem4  24291  logge0b  24377  loggt0b  24378  logle1b  24379  loglt1b  24380  atanord  24654  rlimcnp2  24693  bposlem7  25015  lgsprme0  25064  rpvmasum2  25201  trgcgrg  25410  legov3  25493  opphllem6  25644  ebtwntg  25862  wwlksm1edg  26767  hial2eq2  27964  adjsym  28692  cnvadj  28751  eigvalcl  28820  mddmd  29160  mdslmd2i  29189  elat2  29199  xdivpnfrp  29641  isorng  29799  unitdivcld  29947  indpreima  30087  ioosconn  31229  pdivsq  31635  poimirlem26  33435  areacirclem1  33500  isat3  34594  ishlat3N  34641  cvrval5  34701  llnexchb2  35155  lhpoc2N  35301  lhprelat3N  35326  lautcnvle  35375  lautcvr  35378  ltrncnvatb  35424  cdlemb3  35894  cdlemg17h  35956  dih0vbN  36571  djhcvat42  36704  dvh4dimat  36727  mapdordlem2  36926  diophun  37337  jm2.19lem4  37559  uneqsn  38321  xrralrecnnge  39613  limsupre2lem  39956  flsqrt5  41509  isrnghm  41892  lincfsuppcl  42202