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  813  biassdc  1373  pm5.24dc  1376  anxordi  1378  sbequ12a  1746  drex1  1770  sbcomxyyz  1943  sb9v  1951  csbiebt  3034  prsspwg  3674  bnd2  4092  copsex2t  4162  copsex2g  4163  fnssresb  5230  fcnvres  5301  dmfco  5482  funimass5  5530  fmptco  5579  cbvfo  5679  cbvexfo  5680  isocnv  5705  isoini  5712  isoselem  5714  riota2df  5743  ovmpodxf  5889  caovcanrd  5927  fidcenumlemrks  6834  ordiso2  6913  ltpiord  7120  dfplpq2  7155  dfmpq2  7156  enqeceq  7160  enq0eceq  7238  enreceq  7537  ltpsrprg  7604  mappsrprg  7605  cnegexlem3  7932  subeq0  7981  negcon1  8007  subexsub  8127  subeqrev  8131  lesub  8196  ltsub13  8198  subge0  8230  div11ap  8453  divmuleqap  8470  ltmuldiv2  8626  lemuldiv2  8633  nn1suc  8732  addltmul  8949  elnnnn0  9013  znn0sub  9112  prime  9143  indstr  9381  qapne  9424  qlttri2  9426  fz1n  9817  fzrev3  9860  fzonlt0  9937  divfl0  10062  modqsubdir  10159  fzfig  10196  sqrt11  10804  sqrtsq2  10808  absdiflt  10857  absdifle  10858  nnabscl  10865  minclpr  11001  xrnegiso  11024  xrnegcon1d  11026  clim2  11045  climshft2  11068  sumrbdc  11140  prodrbdclem2  11335  sinbnd  11448  cosbnd  11449  dvdscmulr  11511  dvdsmulcr  11512  oddm1even  11561  qredeq  11766  cncongr2  11774  isprm3  11788  prmrp  11812  sqrt2irr  11829  crth  11889  eltg3  12215  eltop  12227  eltop2  12228  eltop3  12229  lmbrf  12373  cncnpi  12386  txcn  12433  hmeoimaf1o  12472  ismet2  12512  xmseq0  12626