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  829  biassdc  1406  pm5.24dc  1409  anxordi  1411  sbequ12a  1784  drex1  1809  sbcomxyyz  1988  sb9v  1994  csbiebt  3120  prsspwg  3778  bnd2  4202  copsex2t  4274  copsex2g  4275  fnssresb  5366  fcnvres  5437  foelcdmi  5609  dmfco  5625  funimass5  5675  fmptco  5724  cbvfo  5828  cbvexfo  5829  isocnv  5854  isoini  5861  isoselem  5863  riota2df  5894  ovmpodxf  6044  caovcanrd  6082  fidcenumlemrks  7012  ordiso2  7094  ltpiord  7379  dfplpq2  7414  dfmpq2  7415  enqeceq  7419  enq0eceq  7497  enreceq  7796  ltpsrprg  7863  mappsrprg  7864  cnegexlem3  8196  subeq0  8245  negcon1  8271  subexsub  8391  subeqrev  8395  lesub  8460  ltsub13  8462  subge0  8494  div11ap  8719  divmuleqap  8736  ltmuldiv2  8894  lemuldiv2  8901  nn1suc  9001  addltmul  9219  elnnnn0  9283  znn0sub  9382  prime  9416  indstr  9658  qapne  9704  qlttri2  9706  fz1n  10110  fzrev3  10153  fzonlt0  10234  divfl0  10365  modqsubdir  10464  fzfig  10501  wrdlenge1n0  10947  sqrt11  11183  sqrtsq2  11187  absdiflt  11236  absdifle  11237  nnabscl  11244  minclpr  11380  xrnegiso  11405  xrnegcon1d  11407  clim2  11426  climshft2  11449  sumrbdc  11522  prodrbdclem2  11716  fprodssdc  11733  sinbnd  11895  cosbnd  11896  dvdscmulr  11963  dvdsmulcr  11964  oddm1even  12016  qredeq  12234  cncongr2  12242  isprm3  12256  prmrp  12283  sqrt2irr  12300  crth  12362  pcdvdsb  12458  ssnnctlemct  12603  xpsfrnel2  12929  gsumval2  12980  grpid  13111  grpidrcan  13137  grpidlcan  13138  grplmulf1o  13146  imasgrp2  13180  ghmeqker  13341  abladdsub4  13384  imasrng  13452  imasring  13560  lspsnss2  13915  znf1o  14139  znidom  14145  znunit  14147  znrrg  14148  eltg3  14225  eltop  14237  eltop2  14238  eltop3  14239  lmbrf  14383  cncnpi  14396  txcn  14443  hmeoimaf1o  14482  ismet2  14522  xmseq0  14636  wilthlem1  15112  lgsne0  15154  lgsquadlem1  15191  2sqlem7  15208