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  828  biassdc  1395  pm5.24dc  1398  anxordi  1400  sbequ12a  1773  drex1  1798  sbcomxyyz  1972  sb9v  1978  csbiebt  3097  prsspwg  3753  bnd2  4174  copsex2t  4246  copsex2g  4247  fnssresb  5329  fcnvres  5400  foelcdmi  5569  dmfco  5585  funimass5  5634  fmptco  5683  cbvfo  5786  cbvexfo  5787  isocnv  5812  isoini  5819  isoselem  5821  riota2df  5851  ovmpodxf  6000  caovcanrd  6038  fidcenumlemrks  6952  ordiso2  7034  ltpiord  7318  dfplpq2  7353  dfmpq2  7354  enqeceq  7358  enq0eceq  7436  enreceq  7735  ltpsrprg  7802  mappsrprg  7803  cnegexlem3  8134  subeq0  8183  negcon1  8209  subexsub  8329  subeqrev  8333  lesub  8398  ltsub13  8400  subge0  8432  div11ap  8657  divmuleqap  8674  ltmuldiv2  8832  lemuldiv2  8839  nn1suc  8938  addltmul  9155  elnnnn0  9219  znn0sub  9318  prime  9352  indstr  9593  qapne  9639  qlttri2  9641  fz1n  10044  fzrev3  10087  fzonlt0  10167  divfl0  10296  modqsubdir  10393  fzfig  10430  sqrt11  11048  sqrtsq2  11052  absdiflt  11101  absdifle  11102  nnabscl  11109  minclpr  11245  xrnegiso  11270  xrnegcon1d  11272  clim2  11291  climshft2  11314  sumrbdc  11387  prodrbdclem2  11581  fprodssdc  11598  sinbnd  11760  cosbnd  11761  dvdscmulr  11827  dvdsmulcr  11828  oddm1even  11880  qredeq  12096  cncongr2  12104  isprm3  12118  prmrp  12145  sqrt2irr  12162  crth  12224  pcdvdsb  12319  ssnnctlemct  12447  xpsfrnel2  12765  grpid  12912  grpidrcan  12935  grpidlcan  12936  grplmulf1o  12944  abladdsub4  13117  eltg3  13560  eltop  13572  eltop2  13573  eltop3  13574  lmbrf  13718  cncnpi  13731  txcn  13778  hmeoimaf1o  13817  ismet2  13857  xmseq0  13971  lgsne0  14442  2sqlem7  14471