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  835  biassdc  1439  pm5.24dc  1442  anxordi  1444  sbequ12a  1821  drex1  1846  sbcomxyyz  2025  sb9v  2031  csbiebt  3167  prsspwg  3833  ssprss  3834  bnd2  4263  copsex2t  4337  copsex2g  4338  fnssresb  5444  fcnvres  5520  foelcdmi  5698  dmfco  5714  funimass5  5764  fmptco  5813  cbvfo  5926  cbvexfo  5927  isocnv  5952  isoini  5959  isoselem  5961  riota2df  5993  ovmpodxf  6147  caovcanrd  6186  fidcenumlemrks  7152  ordiso2  7234  ltpiord  7539  dfplpq2  7574  dfmpq2  7575  enqeceq  7579  enq0eceq  7657  enreceq  7956  ltpsrprg  8023  mappsrprg  8024  cnegexlem3  8356  subeq0  8405  negcon1  8431  subexsub  8551  subeqrev  8555  lesub  8621  ltsub13  8623  subge0  8655  div11ap  8880  divmuleqap  8897  ltmuldiv2  9055  lemuldiv2  9062  nn1suc  9162  addltmul  9381  elnnnn0  9445  znn0sub  9545  prime  9579  indstr  9827  qapne  9873  qlttri2  9875  fz1n  10279  fzrev3  10322  fzo0n  10403  fzonlt0  10404  divfl0  10557  modqsubdir  10656  fzfig  10693  wrdlenge1n0  11148  pfxccat3a  11320  sqrt11  11601  sqrtsq2  11605  absdiflt  11654  absdifle  11655  nnabscl  11662  minclpr  11799  xrnegiso  11824  xrnegcon1d  11826  clim2  11845  climshft2  11868  sumrbdc  11942  prodrbdclem2  12136  fprodssdc  12153  sinbnd  12315  cosbnd  12316  dvdscmulr  12383  dvdsmulcr  12384  oddm1even  12438  bitsmod  12519  bitsinv1lem  12524  qredeq  12670  cncongr2  12678  isprm3  12692  prmrp  12719  sqrt2irr  12736  crth  12798  pcdvdsb  12895  ssnnctlemct  13069  pwselbasb  13378  xpsfrnel2  13431  gsumval2  13482  imasmnd2  13537  grpid  13624  grpidrcan  13650  grpidlcan  13651  grplmulf1o  13659  imasgrp2  13699  ghmeqker  13860  abladdsub4  13903  imasrng  13972  imasring  14080  lspsnss2  14436  znf1o  14668  znidom  14674  znunit  14676  znrrg  14677  eltg3  14784  eltop  14796  eltop2  14797  eltop3  14798  lmbrf  14942  cncnpi  14955  txcn  15002  hmeoimaf1o  15041  ismet2  15081  xmseq0  15195  wilthlem1  15707  fsumdvdsmul  15718  lgsne0  15770  lgsquadlem1  15809  lgsquadlem2  15810  2sqlem7  15853  clwwlkn1  16272  eupth2lem2dc  16313  eupth2lem3lem3fi  16324  eupth2lem3lem6fi  16325