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  6420  enreceq  6664  cnegexlem3  6985  subeq0  7033  negcon1  7059  subeqrev  7170  lesub  7231  ltsub13  7233  subge0  7265  div11ap  7459  divmuleqap  7475  ltmuldiv2  7622  lemuldiv2  7629  nn1suc  7714  addltmul  7938  elnnnn0  8001  znn0sub  8085  prime  8113  indstr  8312  qapne  8350  fz1n  8678  fzrev3  8719  fzonlt0  8793  fzfig  8887