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  832  biassdc  1417  pm5.24dc  1420  anxordi  1422  sbequ12a  1799  drex1  1824  sbcomxyyz  2003  sb9v  2009  csbiebt  3144  prsspwg  3807  ssprss  3808  bnd2  4236  copsex2t  4310  copsex2g  4311  fnssresb  5411  fcnvres  5485  foelcdmi  5659  dmfco  5675  funimass5  5725  fmptco  5774  cbvfo  5882  cbvexfo  5883  isocnv  5908  isoini  5915  isoselem  5917  riota2df  5949  ovmpodxf  6101  caovcanrd  6140  fidcenumlemrks  7088  ordiso2  7170  ltpiord  7474  dfplpq2  7509  dfmpq2  7510  enqeceq  7514  enq0eceq  7592  enreceq  7891  ltpsrprg  7958  mappsrprg  7959  cnegexlem3  8291  subeq0  8340  negcon1  8366  subexsub  8486  subeqrev  8490  lesub  8556  ltsub13  8558  subge0  8590  div11ap  8815  divmuleqap  8832  ltmuldiv2  8990  lemuldiv2  8997  nn1suc  9097  addltmul  9316  elnnnn0  9380  znn0sub  9480  prime  9514  indstr  9756  qapne  9802  qlttri2  9804  fz1n  10208  fzrev3  10251  fzo0n  10332  fzonlt0  10333  divfl0  10483  modqsubdir  10582  fzfig  10619  wrdlenge1n0  11071  pfxccat3a  11236  sqrt11  11516  sqrtsq2  11520  absdiflt  11569  absdifle  11570  nnabscl  11577  minclpr  11714  xrnegiso  11739  xrnegcon1d  11741  clim2  11760  climshft2  11783  sumrbdc  11856  prodrbdclem2  12050  fprodssdc  12067  sinbnd  12229  cosbnd  12230  dvdscmulr  12297  dvdsmulcr  12298  oddm1even  12352  bitsmod  12433  bitsinv1lem  12438  qredeq  12584  cncongr2  12592  isprm3  12606  prmrp  12633  sqrt2irr  12650  crth  12712  pcdvdsb  12809  ssnnctlemct  12983  pwselbasb  13292  xpsfrnel2  13345  gsumval2  13396  imasmnd2  13451  grpid  13538  grpidrcan  13564  grpidlcan  13565  grplmulf1o  13573  imasgrp2  13613  ghmeqker  13774  abladdsub4  13817  imasrng  13885  imasring  13993  lspsnss2  14348  znf1o  14580  znidom  14586  znunit  14588  znrrg  14589  eltg3  14696  eltop  14708  eltop2  14709  eltop3  14710  lmbrf  14854  cncnpi  14867  txcn  14914  hmeoimaf1o  14953  ismet2  14993  xmseq0  15107  wilthlem1  15619  fsumdvdsmul  15630  lgsne0  15682  lgsquadlem1  15721  lgsquadlem2  15722  2sqlem7  15765