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  4257  copsex2t  4331  copsex2g  4332  fnssresb  5435  fcnvres  5511  foelcdmi  5688  dmfco  5704  funimass5  5754  fmptco  5803  cbvfo  5915  cbvexfo  5916  isocnv  5941  isoini  5948  isoselem  5950  riota2df  5982  ovmpodxf  6136  caovcanrd  6175  fidcenumlemrks  7128  ordiso2  7210  ltpiord  7514  dfplpq2  7549  dfmpq2  7550  enqeceq  7554  enq0eceq  7632  enreceq  7931  ltpsrprg  7998  mappsrprg  7999  cnegexlem3  8331  subeq0  8380  negcon1  8406  subexsub  8526  subeqrev  8530  lesub  8596  ltsub13  8598  subge0  8630  div11ap  8855  divmuleqap  8872  ltmuldiv2  9030  lemuldiv2  9037  nn1suc  9137  addltmul  9356  elnnnn0  9420  znn0sub  9520  prime  9554  indstr  9796  qapne  9842  qlttri2  9844  fz1n  10248  fzrev3  10291  fzo0n  10372  fzonlt0  10373  divfl0  10524  modqsubdir  10623  fzfig  10660  wrdlenge1n0  11113  pfxccat3a  11278  sqrt11  11558  sqrtsq2  11562  absdiflt  11611  absdifle  11612  nnabscl  11619  minclpr  11756  xrnegiso  11781  xrnegcon1d  11783  clim2  11802  climshft2  11825  sumrbdc  11898  prodrbdclem2  12092  fprodssdc  12109  sinbnd  12271  cosbnd  12272  dvdscmulr  12339  dvdsmulcr  12340  oddm1even  12394  bitsmod  12475  bitsinv1lem  12480  qredeq  12626  cncongr2  12634  isprm3  12648  prmrp  12675  sqrt2irr  12692  crth  12754  pcdvdsb  12851  ssnnctlemct  13025  pwselbasb  13334  xpsfrnel2  13387  gsumval2  13438  imasmnd2  13493  grpid  13580  grpidrcan  13606  grpidlcan  13607  grplmulf1o  13615  imasgrp2  13655  ghmeqker  13816  abladdsub4  13859  imasrng  13927  imasring  14035  lspsnss2  14391  znf1o  14623  znidom  14629  znunit  14631  znrrg  14632  eltg3  14739  eltop  14751  eltop2  14752  eltop3  14753  lmbrf  14897  cncnpi  14910  txcn  14957  hmeoimaf1o  14996  ismet2  15036  xmseq0  15150  wilthlem1  15662  fsumdvdsmul  15673  lgsne0  15725  lgsquadlem1  15764  lgsquadlem2  15765  2sqlem7  15808