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  3181  prsspwg  3859  ssprss  3860  bnd2  4291  copsex2t  4366  copsex2g  4367  fnssresb  5475  fcnvres  5555  foelcdmi  5734  dmfco  5750  funimass5  5800  fmptco  5848  cbvfo  5964  cbvexfo  5965  isocnv  5990  isoini  5997  isoselem  5999  riota2df  6033  ovmpodxf  6187  caovcanrd  6226  suppimacnvfn  6459  fidcenumlemrks  7236  ordiso2  7339  ltpiord  7650  dfplpq2  7685  dfmpq2  7686  enqeceq  7690  enq0eceq  7768  enreceq  8067  ltpsrprg  8134  mappsrprg  8135  cnegexlem3  8467  subeq0  8516  negcon1  8542  subexsub  8662  subeqrev  8666  lesub  8733  ltsub13  8735  subge0  8767  div11ap  8994  divmuleqap  9011  ltmuldiv2  9169  lemuldiv2  9176  nn1suc  9276  addltmul  9495  elnnnn0  9559  znn0sub  9663  prime  9698  indstr  9946  qapne  9992  qlttri2  9994  fz1n  10401  fzrev3  10446  fzo0n  10527  fzonlt0  10528  divfl0  10683  modqsubdir  10782  fzfig  10819  wrdlenge1n0  11286  pfxccat3a  11458  sqrt11  11752  sqrtsq2  11756  absdiflt  11805  absdifle  11806  nnabscl  11813  minclpr  11950  xrnegiso  11975  xrnegcon1d  11977  clim2  11996  climshft2  12019  sumrbdc  12093  prodrbdclem2  12287  fprodssdc  12304  sinbnd  12466  cosbnd  12467  dvdscmulr  12534  dvdsmulcr  12535  oddm1even  12589  bitsmod  12670  bitsinv1lem  12675  qredeq  12821  cncongr2  12829  isprm3  12843  prmrp  12870  sqrt2irr  12887  crth  12949  pcdvdsb  13046  ballotfilemfc0  13179  ballotfilemfcc  13180  ssnnctlemct  13284  xpsfrnel2  13613  gsumval2  13663  imasmnd2  13710  grpid  13797  grpidrcan  13823  grpidlcan  13824  grplmulf1o  13832  imasgrp2  13866  ghmeqker  14027  abladdsub4  14070  pwselbasb  14151  imasrng  14198  imasring  14310  lspsnss2  14696  znf1o  14928  znidom  14934  znunit  14936  znrrg  14937  eltg3  15051  eltop  15063  eltop2  15064  eltop3  15065  lmbrf  15209  cncnpi  15222  txcn  15269  hmeoimaf1o  15308  ismet2  15348  xmseq0  15462  wilthlem1  15977  fsumdvdsmul  15988  lgsne0  16040  lgsquadlem1  16079  lgsquadlem2  16080  2sqlem7  16123  clwwlkn1  16542  eupth2lem2dc  16583  eupth2lem3lem3fi  16594  eupth2lem3lem6fi  16595