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  1945  sb9v  1953  csbiebt  3039  prsspwg  3679  bnd2  4097  copsex2t  4167  copsex2g  4168  fnssresb  5235  fcnvres  5306  dmfco  5489  funimass5  5537  fmptco  5586  cbvfo  5686  cbvexfo  5687  isocnv  5712  isoini  5719  isoselem  5721  riota2df  5750  ovmpodxf  5896  caovcanrd  5934  fidcenumlemrks  6841  ordiso2  6920  ltpiord  7134  dfplpq2  7169  dfmpq2  7170  enqeceq  7174  enq0eceq  7252  enreceq  7551  ltpsrprg  7618  mappsrprg  7619  cnegexlem3  7946  subeq0  7995  negcon1  8021  subexsub  8141  subeqrev  8145  lesub  8210  ltsub13  8212  subge0  8244  div11ap  8467  divmuleqap  8484  ltmuldiv2  8640  lemuldiv2  8647  nn1suc  8746  addltmul  8963  elnnnn0  9027  znn0sub  9126  prime  9157  indstr  9395  qapne  9438  qlttri2  9440  fz1n  9831  fzrev3  9874  fzonlt0  9951  divfl0  10076  modqsubdir  10173  fzfig  10210  sqrt11  10818  sqrtsq2  10822  absdiflt  10871  absdifle  10872  nnabscl  10879  minclpr  11015  xrnegiso  11038  xrnegcon1d  11040  clim2  11059  climshft2  11082  sumrbdc  11155  prodrbdclem2  11349  sinbnd  11466  cosbnd  11467  dvdscmulr  11529  dvdsmulcr  11530  oddm1even  11579  qredeq  11784  cncongr2  11792  isprm3  11806  prmrp  11830  sqrt2irr  11847  crth  11907  eltg3  12236  eltop  12248  eltop2  12249  eltop3  12250  lmbrf  12394  cncnpi  12407  txcn  12454  hmeoimaf1o  12493  ismet2  12533  xmseq0  12647