Theorem bitr2d 262

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

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

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 190

This theorem is referenced by:  3bitrrd  288  3bitr2rd  290  pm5.18  362  ifptru  1446  sbequ12a  2095  elrnmpt1  5101  fndmdif  6008  weniso  6269  sbcopeq1a  6871  cfss  8720  posdif  10134  lesub1  10135  lesub0  10158  ltdivmul  10507  ledivmul  10508  zlem1lt  11016  zltlem1  11017  negelrp  11361  ioon0  11690  fzn  11843  fzrev2  11887  fz1sbc  11898  elfzp1b  11899  sumsqeq0  12384  hashfzdm  12644  hashfirdm  12646  fz1isolem  12656  sqrtle  13372  absgt0  13435  isershft  13775  incexc2  13944  dvdssubr  14394  gcdn0gt0  14534  pcfac  14892  ramval  15008  ramvalOLD  15009  ltbwe  18744  iunocv  19292  lmbrf  20324  perfcls  20429  ovolscalem1  22514  itg2mulclem  22752  sineq0  23524  efif1olem4  23542  atanord  23901  rlimcnp2  23940  bposlem7  24266  rpvmasum2  24398  trgcgrg  24608  legov3  24691  opphllem6  24842  ebtwntg  25060  wwlkm1edg  25511  usg2spthonot0  25665  hial2eq2  26808  adjsym  27534  cnvadj  27593  eigvalcl  27662  mddmd  28002  mdslmd2i  28031  elat2  28041  xdivpnfrp  28450  isorng  28610  unitdivcld  28755  indpreima  28894  iooscon  30018  possumd  30414  pdivsq  30433  poimirlem26  32010  areacirclem1  32076  isat3  32917  ishlat3N  32964  cvrval5  33024  llnexchb2  33478  lhpoc2N  33624  lhprelat3N  33649  lautcnvle  33698  lautcvr  33701  ltrncnvatb  33747  cdlemb3  34217  cdlemg17h  34279  dih0vbN  34894  djhcvat42  35027  dvh4dimat  35050  mapdordlem2  35249  diophun  35660  jm2.19lem4  35891  isrnghm  40164  lincfsuppcl  40478  logge0b  40614  loggt0b  40615  logle1b  40616  loglt1b  40617