Theorem bitr3d 190

Description: Deduction form of bitr3i 186. (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 141	. 2 |- ( ph -> ( ch <-> ps ) )
3		bitr3d.2	. 2 |- ( ph -> ( ps <-> th ) )
4	2, 3	bitrd 188	1 |- ( ph -> ( ch <-> th ) )

Syntax hints:   -> wi 4   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3bitrrd  215  3bitr3d  218  3bitr3rd  219  pm5.16  833  biassdc  1437  pm5.24dc  1440  anxordi  1442  sbequ12a  1819  drex1  1844  sbcomxyyz  2023  sb9v  2029  csbiebt  3164  prsspwg  3828  ssprss  3829  bnd2  4258  copsex2t  4332  copsex2g  4333  fnssresb  5438  fcnvres  5514  foelcdmi  5691  dmfco  5707  funimass5  5757  fmptco  5806  cbvfo  5918  cbvexfo  5919  isocnv  5944  isoini  5951  isoselem  5953  riota2df  5985  ovmpodxf  6139  caovcanrd  6178  fidcenumlemrks  7136  ordiso2  7218  ltpiord  7522  dfplpq2  7557  dfmpq2  7558  enqeceq  7562  enq0eceq  7640  enreceq  7939  ltpsrprg  8006  mappsrprg  8007  cnegexlem3  8339  subeq0  8388  negcon1  8414  subexsub  8534  subeqrev  8538  lesub  8604  ltsub13  8606  subge0  8638  div11ap  8863  divmuleqap  8880  ltmuldiv2  9038  lemuldiv2  9045  nn1suc  9145  addltmul  9364  elnnnn0  9428  znn0sub  9528  prime  9562  indstr  9805  qapne  9851  qlttri2  9853  fz1n  10257  fzrev3  10300  fzo0n  10381  fzonlt0  10382  divfl0  10533  modqsubdir  10632  fzfig  10669  wrdlenge1n0  11123  pfxccat3a  11291  sqrt11  11571  sqrtsq2  11575  absdiflt  11624  absdifle  11625  nnabscl  11632  minclpr  11769  xrnegiso  11794  xrnegcon1d  11796  clim2  11815  climshft2  11838  sumrbdc  11911  prodrbdclem2  12105  fprodssdc  12122  sinbnd  12284  cosbnd  12285  dvdscmulr  12352  dvdsmulcr  12353  oddm1even  12407  bitsmod  12488  bitsinv1lem  12493  qredeq  12639  cncongr2  12647  isprm3  12661  prmrp  12688  sqrt2irr  12705  crth  12767  pcdvdsb  12864  ssnnctlemct  13038  pwselbasb  13347  xpsfrnel2  13400  gsumval2  13451  imasmnd2  13506  grpid  13593  grpidrcan  13619  grpidlcan  13620  grplmulf1o  13628  imasgrp2  13668  ghmeqker  13829  abladdsub4  13872  imasrng  13940  imasring  14048  lspsnss2  14404  znf1o  14636  znidom  14642  znunit  14644  znrrg  14645  eltg3  14752  eltop  14764  eltop2  14765  eltop3  14766  lmbrf  14910  cncnpi  14923  txcn  14970  hmeoimaf1o  15009  ismet2  15049  xmseq0  15163  wilthlem1  15675  fsumdvdsmul  15686  lgsne0  15738  lgsquadlem1  15777  lgsquadlem2  15778  2sqlem7  15821  clwwlkn1  16186