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  829  biassdc  1406  pm5.24dc  1409  anxordi  1411  sbequ12a  1787  drex1  1812  sbcomxyyz  1991  sb9v  1997  csbiebt  3124  prsspwg  3783  bnd2  4207  copsex2t  4279  copsex2g  4280  fnssresb  5373  fcnvres  5444  foelcdmi  5616  dmfco  5632  funimass5  5682  fmptco  5731  cbvfo  5835  cbvexfo  5836  isocnv  5861  isoini  5868  isoselem  5870  riota2df  5901  ovmpodxf  6052  caovcanrd  6091  fidcenumlemrks  7028  ordiso2  7110  ltpiord  7403  dfplpq2  7438  dfmpq2  7439  enqeceq  7443  enq0eceq  7521  enreceq  7820  ltpsrprg  7887  mappsrprg  7888  cnegexlem3  8220  subeq0  8269  negcon1  8295  subexsub  8415  subeqrev  8419  lesub  8485  ltsub13  8487  subge0  8519  div11ap  8744  divmuleqap  8761  ltmuldiv2  8919  lemuldiv2  8926  nn1suc  9026  addltmul  9245  elnnnn0  9309  znn0sub  9408  prime  9442  indstr  9684  qapne  9730  qlttri2  9732  fz1n  10136  fzrev3  10179  fzonlt0  10260  divfl0  10403  modqsubdir  10502  fzfig  10539  wrdlenge1n0  10985  sqrt11  11221  sqrtsq2  11225  absdiflt  11274  absdifle  11275  nnabscl  11282  minclpr  11419  xrnegiso  11444  xrnegcon1d  11446  clim2  11465  climshft2  11488  sumrbdc  11561  prodrbdclem2  11755  fprodssdc  11772  sinbnd  11934  cosbnd  11935  dvdscmulr  12002  dvdsmulcr  12003  oddm1even  12057  bitsmod  12138  bitsinv1lem  12143  qredeq  12289  cncongr2  12297  isprm3  12311  prmrp  12338  sqrt2irr  12355  crth  12417  pcdvdsb  12514  ssnnctlemct  12688  pwselbasb  12995  xpsfrnel2  13048  gsumval2  13099  imasmnd2  13154  grpid  13241  grpidrcan  13267  grpidlcan  13268  grplmulf1o  13276  imasgrp2  13316  ghmeqker  13477  abladdsub4  13520  imasrng  13588  imasring  13696  lspsnss2  14051  znf1o  14283  znidom  14289  znunit  14291  znrrg  14292  eltg3  14377  eltop  14389  eltop2  14390  eltop3  14391  lmbrf  14535  cncnpi  14548  txcn  14595  hmeoimaf1o  14634  ismet2  14674  xmseq0  14788  wilthlem1  15300  fsumdvdsmul  15311  lgsne0  15363  lgsquadlem1  15402  lgsquadlem2  15403  2sqlem7  15446