Theorem bitr3d 188

Description: Deduction form of bitr3i 184. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
bitr3d.1	|- ( ph -> ( ps <-> ch ) )
bitr3d.2	|- ( ph -> ( ps <-> th ) )

Assertion

Ref	Expression
bitr3d	|- ( ph -> ( ch <-> th ) )

Proof of Theorem bitr3d

Step	Hyp	Ref	Expression
1		bitr3d.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	bicomd 139	. 2 |- ( ph -> ( ch <-> ps ) )
3		bitr3d.2	. 2 |- ( ph -> ( ps <-> th ) )
4	2, 3	bitrd 186	1 |- ( ph -> ( ch <-> th ) )

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  3bitrrd  213  3bitr3d  216  3bitr3rd  217  pm5.16  770  biassdc  1326  pm5.24dc  1329  anxordi  1331  sbequ12a  1696  drex1  1719  sbcomxyyz  1887  sb9v  1895  csbiebt  2942  prsspwg  3544  bnd2  3947  copsex2t  4000  copsex2g  4001  fnssresb  5031  fcnvres  5093  dmfco  5262  funimass5  5305  fmptco  5351  cbvfo  5445  cbvexfo  5446  isocnv  5471  isoini  5477  isoselem  5479  riota2df  5508  ovmpt2dxf  5646  caovcanrd  5684  ordiso2  6446  ltpiord  6509  dfplpq2  6544  dfmpq2  6545  enqeceq  6549  enq0eceq  6627  enreceq  6913  cnegexlem3  7285  subeq0  7334  negcon1  7360  subexsub  7476  subeqrev  7480  lesub  7545  ltsub13  7547  subge0  7579  div11ap  7788  divmuleqap  7805  ltmuldiv2  7953  lemuldiv2  7960  nn1suc  8058  addltmul  8267  elnnnn0  8331  znn0sub  8416  prime  8446  indstr  8681  qapne  8724  qlttri2  8726  fz1n  9063  fzrev3  9104  fzonlt0  9176  divfl0  9298  modqsubdir  9395  fzfig  9422  sqrt11  9925  sqrtsq2  9929  absdiflt  9978  absdifle  9979  nnabscl  9986  clim2  10122  climshft2  10145  dvdscmulr  10224  dvdsmulcr  10225  oddm1even  10274  qredeq  10478  cncongr2  10486  isprm3  10500  prmrp  10524  sqrt2irr  10541