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  5509  foelcdmi  5686  dmfco  5702  funimass5  5752  fmptco  5801  cbvfo  5909  cbvexfo  5910  isocnv  5935  isoini  5942  isoselem  5944  riota2df  5976  ovmpodxf  6130  caovcanrd  6169  fidcenumlemrks  7120  ordiso2  7202  ltpiord  7506  dfplpq2  7541  dfmpq2  7542  enqeceq  7546  enq0eceq  7624  enreceq  7923  ltpsrprg  7990  mappsrprg  7991  cnegexlem3  8323  subeq0  8372  negcon1  8398  subexsub  8518  subeqrev  8522  lesub  8588  ltsub13  8590  subge0  8622  div11ap  8847  divmuleqap  8864  ltmuldiv2  9022  lemuldiv2  9029  nn1suc  9129  addltmul  9348  elnnnn0  9412  znn0sub  9512  prime  9546  indstr  9788  qapne  9834  qlttri2  9836  fz1n  10240  fzrev3  10283  fzo0n  10364  fzonlt0  10365  divfl0  10516  modqsubdir  10615  fzfig  10652  wrdlenge1n0  11105  pfxccat3a  11270  sqrt11  11550  sqrtsq2  11554  absdiflt  11603  absdifle  11604  nnabscl  11611  minclpr  11748  xrnegiso  11773  xrnegcon1d  11775  clim2  11794  climshft2  11817  sumrbdc  11890  prodrbdclem2  12084  fprodssdc  12101  sinbnd  12263  cosbnd  12264  dvdscmulr  12331  dvdsmulcr  12332  oddm1even  12386  bitsmod  12467  bitsinv1lem  12472  qredeq  12618  cncongr2  12626  isprm3  12640  prmrp  12667  sqrt2irr  12684  crth  12746  pcdvdsb  12843  ssnnctlemct  13017  pwselbasb  13326  xpsfrnel2  13379  gsumval2  13430  imasmnd2  13485  grpid  13572  grpidrcan  13598  grpidlcan  13599  grplmulf1o  13607  imasgrp2  13647  ghmeqker  13808  abladdsub4  13851  imasrng  13919  imasring  14027  lspsnss2  14383  znf1o  14615  znidom  14621  znunit  14623  znrrg  14624  eltg3  14731  eltop  14743  eltop2  14744  eltop3  14745  lmbrf  14889  cncnpi  14902  txcn  14949  hmeoimaf1o  14988  ismet2  15028  xmseq0  15142  wilthlem1  15654  fsumdvdsmul  15665  lgsne0  15717  lgsquadlem1  15756  lgsquadlem2  15757  2sqlem7  15800