Theorem bitr3d 189

Description: Deduction form of bitr3i 185. (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 140	. 2 |- ( ph -> ( ch <-> ps ) )
3		bitr3d.2	. 2 |- ( ph -> ( ps <-> th ) )
4	2, 3	bitrd 187	1 |- ( ph -> ( ch <-> th ) )

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3bitrrd  214  3bitr3d  217  3bitr3rd  218  pm5.16  796  biassdc  1354  pm5.24dc  1357  anxordi  1359  sbequ12a  1727  drex1  1750  sbcomxyyz  1919  sb9v  1927  csbiebt  3003  prsspwg  3643  bnd2  4055  copsex2t  4125  copsex2g  4126  fnssresb  5191  fcnvres  5262  dmfco  5441  funimass5  5489  fmptco  5538  cbvfo  5638  cbvexfo  5639  isocnv  5664  isoini  5671  isoselem  5673  riota2df  5702  ovmpodxf  5848  caovcanrd  5886  fidcenumlemrks  6791  ordiso2  6870  ltpiord  7069  dfplpq2  7104  dfmpq2  7105  enqeceq  7109  enq0eceq  7187  enreceq  7473  cnegexlem3  7856  subeq0  7905  negcon1  7931  subexsub  8047  subeqrev  8051  lesub  8116  ltsub13  8118  subge0  8150  div11ap  8367  divmuleqap  8384  ltmuldiv2  8537  lemuldiv2  8544  nn1suc  8643  addltmul  8854  elnnnn0  8918  znn0sub  9017  prime  9048  indstr  9284  qapne  9327  qlttri2  9329  fz1n  9711  fzrev3  9754  fzonlt0  9831  divfl0  9956  modqsubdir  10053  fzfig  10090  sqrt11  10697  sqrtsq2  10701  absdiflt  10750  absdifle  10751  nnabscl  10758  minclpr  10894  xrnegiso  10917  xrnegcon1d  10919  clim2  10938  climshft2  10961  sumrbdc  11033  sinbnd  11304  cosbnd  11305  dvdscmulr  11364  dvdsmulcr  11365  oddm1even  11414  qredeq  11617  cncongr2  11625  isprm3  11639  prmrp  11663  sqrt2irr  11680  crth  11739  eltg3  12063  eltop  12075  eltop2  12076  eltop3  12077  lmbrf  12220  cncnpi  12233  txcn  12280  ismet2  12337  xmseq0  12451