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  1820  drex1  1845  sbcomxyyz  2024  sb9v  2030  csbiebt  3166  prsspwg  3834  ssprss  3835  bnd2  4265  copsex2t  4339  copsex2g  4340  fnssresb  5446  fcnvres  5522  foelcdmi  5701  dmfco  5717  funimass5  5767  fmptco  5816  cbvfo  5931  cbvexfo  5932  isocnv  5957  isoini  5964  isoselem  5966  riota2df  5998  ovmpodxf  6152  caovcanrd  6191  fidcenumlemrks  7157  ordiso2  7239  ltpiord  7544  dfplpq2  7579  dfmpq2  7580  enqeceq  7584  enq0eceq  7662  enreceq  7961  ltpsrprg  8028  mappsrprg  8029  cnegexlem3  8361  subeq0  8410  negcon1  8436  subexsub  8556  subeqrev  8560  lesub  8626  ltsub13  8628  subge0  8660  div11ap  8885  divmuleqap  8902  ltmuldiv2  9060  lemuldiv2  9067  nn1suc  9167  addltmul  9386  elnnnn0  9450  znn0sub  9550  prime  9584  indstr  9832  qapne  9878  qlttri2  9880  fz1n  10284  fzrev3  10327  fzo0n  10408  fzonlt0  10409  divfl0  10562  modqsubdir  10661  fzfig  10698  wrdlenge1n0  11156  pfxccat3a  11328  sqrt11  11622  sqrtsq2  11626  absdiflt  11675  absdifle  11676  nnabscl  11683  minclpr  11820  xrnegiso  11845  xrnegcon1d  11847  clim2  11866  climshft2  11889  sumrbdc  11963  prodrbdclem2  12157  fprodssdc  12174  sinbnd  12336  cosbnd  12337  dvdscmulr  12404  dvdsmulcr  12405  oddm1even  12459  bitsmod  12540  bitsinv1lem  12545  qredeq  12691  cncongr2  12699  isprm3  12713  prmrp  12740  sqrt2irr  12757  crth  12819  pcdvdsb  12916  ssnnctlemct  13090  pwselbasb  13399  xpsfrnel2  13452  gsumval2  13503  imasmnd2  13558  grpid  13645  grpidrcan  13671  grpidlcan  13672  grplmulf1o  13680  imasgrp2  13720  ghmeqker  13881  abladdsub4  13924  imasrng  13993  imasring  14101  lspsnss2  14457  znf1o  14689  znidom  14695  znunit  14697  znrrg  14698  eltg3  14810  eltop  14822  eltop2  14823  eltop3  14824  lmbrf  14968  cncnpi  14981  txcn  15028  hmeoimaf1o  15067  ismet2  15107  xmseq0  15221  wilthlem1  15733  fsumdvdsmul  15744  lgsne0  15796  lgsquadlem1  15835  lgsquadlem2  15836  2sqlem7  15879  clwwlkn1  16298  eupth2lem2dc  16339  eupth2lem3lem3fi  16350  eupth2lem3lem6fi  16351