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  836  biassdc  1440  pm5.24dc  1443  anxordi  1445  sbequ12a  1822  drex1  1847  sbcomxyyz  2028  sb9v  2034  csbiebt  3180  prsspwg  3856  ssprss  3857  bnd2  4288  copsex2t  4363  copsex2g  4364  fnssresb  5472  fcnvres  5552  foelcdmi  5731  dmfco  5747  funimass5  5797  fmptco  5845  cbvfo  5960  cbvexfo  5961  isocnv  5986  isoini  5993  isoselem  5995  riota2df  6027  ovmpodxf  6181  caovcanrd  6220  suppimacnvfn  6448  fidcenumlemrks  7225  ordiso2  7328  ltpiord  7639  dfplpq2  7674  dfmpq2  7675  enqeceq  7679  enq0eceq  7757  enreceq  8056  ltpsrprg  8123  mappsrprg  8124  cnegexlem3  8455  subeq0  8504  negcon1  8530  subexsub  8650  subeqrev  8654  lesub  8720  ltsub13  8722  subge0  8754  div11ap  8979  divmuleqap  8996  ltmuldiv2  9154  lemuldiv2  9161  nn1suc  9261  addltmul  9480  elnnnn0  9544  znn0sub  9648  prime  9683  indstr  9931  qapne  9977  qlttri2  9979  fz1n  10384  fzrev3  10428  fzo0n  10509  fzonlt0  10510  divfl0  10663  modqsubdir  10762  fzfig  10799  wrdlenge1n0  11266  pfxccat3a  11438  sqrt11  11732  sqrtsq2  11736  absdiflt  11785  absdifle  11786  nnabscl  11793  minclpr  11930  xrnegiso  11955  xrnegcon1d  11957  clim2  11976  climshft2  11999  sumrbdc  12073  prodrbdclem2  12267  fprodssdc  12284  sinbnd  12446  cosbnd  12447  dvdscmulr  12514  dvdsmulcr  12515  oddm1even  12569  bitsmod  12650  bitsinv1lem  12655  qredeq  12801  cncongr2  12809  isprm3  12823  prmrp  12850  sqrt2irr  12867  crth  12929  pcdvdsb  13026  ballotfilemfc0  13157  ballotfilemfcc  13158  ssnnctlemct  13218  pwselbasb  13527  xpsfrnel2  13580  gsumval2  13631  imasmnd2  13686  grpid  13773  grpidrcan  13799  grpidlcan  13800  grplmulf1o  13808  imasgrp2  13848  ghmeqker  14009  abladdsub4  14052  imasrng  14121  imasring  14229  lspsnss2  14616  znf1o  14848  znidom  14854  znunit  14856  znrrg  14857  eltg3  14971  eltop  14983  eltop2  14984  eltop3  14985  lmbrf  15129  cncnpi  15142  txcn  15189  hmeoimaf1o  15228  ismet2  15268  xmseq0  15382  wilthlem1  15897  fsumdvdsmul  15908  lgsne0  15960  lgsquadlem1  15999  lgsquadlem2  16000  2sqlem7  16043  clwwlkn1  16462  eupth2lem2dc  16503  eupth2lem3lem3fi  16514  eupth2lem3lem6fi  16515