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-mp 5  ax-1 6  ax-2 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  818  biassdc  1385  pm5.24dc  1388  anxordi  1390  sbequ12a  1761  drex1  1786  sbcomxyyz  1960  sb9v  1966  csbiebt  3084  prsspwg  3732  bnd2  4152  copsex2t  4223  copsex2g  4224  fnssresb  5300  fcnvres  5371  dmfco  5554  funimass5  5602  fmptco  5651  cbvfo  5753  cbvexfo  5754  isocnv  5779  isoini  5786  isoselem  5788  riota2df  5818  ovmpodxf  5967  caovcanrd  6005  fidcenumlemrks  6918  ordiso2  7000  ltpiord  7260  dfplpq2  7295  dfmpq2  7296  enqeceq  7300  enq0eceq  7378  enreceq  7677  ltpsrprg  7744  mappsrprg  7745  cnegexlem3  8075  subeq0  8124  negcon1  8150  subexsub  8270  subeqrev  8274  lesub  8339  ltsub13  8341  subge0  8373  div11ap  8596  divmuleqap  8613  ltmuldiv2  8770  lemuldiv2  8777  nn1suc  8876  addltmul  9093  elnnnn0  9157  znn0sub  9256  prime  9290  indstr  9531  qapne  9577  qlttri2  9579  fz1n  9979  fzrev3  10022  fzonlt0  10102  divfl0  10231  modqsubdir  10328  fzfig  10365  sqrt11  10981  sqrtsq2  10985  absdiflt  11034  absdifle  11035  nnabscl  11042  minclpr  11178  xrnegiso  11203  xrnegcon1d  11205  clim2  11224  climshft2  11247  sumrbdc  11320  prodrbdclem2  11514  fprodssdc  11531  sinbnd  11693  cosbnd  11694  dvdscmulr  11760  dvdsmulcr  11761  oddm1even  11812  qredeq  12028  cncongr2  12036  isprm3  12050  prmrp  12077  sqrt2irr  12094  crth  12156  pcdvdsb  12251  ssnnctlemct  12379  eltg3  12707  eltop  12719  eltop2  12720  eltop3  12721  lmbrf  12865  cncnpi  12878  txcn  12925  hmeoimaf1o  12964  ismet2  13004  xmseq0  13118  lgsne0  13589  2sqlem7  13607