Theorem bitr3d 179

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

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  3bitrrd  204  3bitr3d  207  3bitr3rd  208  pm5.16  737  biassdc  1286  pm5.24dc  1289  anxordi  1291  sbequ12a  1656  drex1  1679  sbcomxyyz  1846  sb9v  1854  csbiebt  2886  prsspwg  3523  bnd2  3926  copsex2t  3982  copsex2g  3983  fnssresb  5011  fcnvres  5073  dmfco  5241  funimass5  5284  fmptco  5330  cbvfo  5425  cbvexfo  5426  isocnv  5451  isoini  5457  isoselem  5459  riota2df  5488  ovmpt2dxf  5626  caovcanrd  5664  ordiso2  6357  ltpiord  6417  dfplpq2  6452  dfmpq2  6453  enqeceq  6457  enq0eceq  6535  enreceq  6821  cnegexlem3  7188  subeq0  7237  negcon1  7263  subeqrev  7374  lesub  7436  ltsub13  7438  subge0  7470  div11ap  7677  divmuleqap  7693  ltmuldiv2  7841  lemuldiv2  7848  nn1suc  7933  addltmul  8161  elnnnn0  8225  znn0sub  8309  prime  8337  indstr  8536  qapne  8574  fz1n  8908  fzrev3  8949  fzonlt0  9023  divfl0  9138  fzfig  9206  sqrt11  9637  sqrtsq2  9641  absdiflt  9688  absdifle  9689  nnabscl  9696  clim2  9804  climshft2  9827  sqrt2irr  9878