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  736  biassdc  1283  pm5.24dc  1286  anxordi  1288  sbequ12a  1653  drex1  1676  sbcomxyyz  1843  sb9v  1851  csbiebt  2880  prsspwg  3514  bnd2  3917  copsex2t  3973  copsex2g  3974  fnssresb  4954  fcnvres  5016  dmfco  5184  funimass5  5227  fmptco  5273  cbvfo  5368  cbvexfo  5369  isocnv  5394  isoini  5400  isoselem  5402  riota2df  5431  ovmpt2dxf  5568  caovcanrd  5606  ltpiord  6303  dfplpq2  6338  dfmpq2  6339  enqeceq  6343  enq0eceq  6419  enreceq  6644  cnegexlem3  6965  subeq0  7013  negcon1  7039  subeqrev  7150  lesub  7211  ltsub13  7213  subge0  7245  div11ap  7439  divmuleqap  7455  ltmuldiv2  7602  lemuldiv2  7609  nn1suc  7694  addltmul  7918  elnnnn0  7981  znn0sub  8065  prime  8093  indstr  8292  qapne  8330  fz1n  8658  fzrev3  8699  fzonlt0  8773  fzfig  8867