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  6624  cnegexlem3  6945  subeq0  6993  negcon1  7019  subeqrev  7130  lesub  7191  ltsub13  7193  subge0  7225  div11ap  7419  divmuleqap  7435  ltmuldiv2  7582  lemuldiv2  7589  nn1suc  7674  addltmul  7898  elnnnn0  7961  znn0sub  8045  prime  8073  indstr  8272  qapne  8310  fz1n  8638  fzrev3  8679  fzonlt0  8753  fzfig  8847