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  2026  sb9v  2032  csbiebt  3177  prsspwg  3853  ssprss  3854  bnd2  4285  copsex2t  4360  copsex2g  4361  fnssresb  5469  fcnvres  5549  foelcdmi  5728  dmfco  5744  funimass5  5794  fmptco  5842  cbvfo  5957  cbvexfo  5958  isocnv  5983  isoini  5990  isoselem  5992  riota2df  6024  ovmpodxf  6178  caovcanrd  6217  suppimacnvfn  6445  fidcenumlemrks  7222  ordiso2  7325  ltpiord  7630  dfplpq2  7665  dfmpq2  7666  enqeceq  7670  enq0eceq  7748  enreceq  8047  ltpsrprg  8114  mappsrprg  8115  cnegexlem3  8446  subeq0  8495  negcon1  8521  subexsub  8641  subeqrev  8645  lesub  8711  ltsub13  8713  subge0  8745  div11ap  8970  divmuleqap  8987  ltmuldiv2  9145  lemuldiv2  9152  nn1suc  9252  addltmul  9471  elnnnn0  9535  znn0sub  9639  prime  9673  indstr  9921  qapne  9967  qlttri2  9969  fz1n  10374  fzrev3  10417  fzo0n  10498  fzonlt0  10499  divfl0  10652  modqsubdir  10751  fzfig  10788  wrdlenge1n0  11251  pfxccat3a  11423  sqrt11  11717  sqrtsq2  11721  absdiflt  11770  absdifle  11771  nnabscl  11778  minclpr  11915  xrnegiso  11940  xrnegcon1d  11942  clim2  11961  climshft2  11984  sumrbdc  12058  prodrbdclem2  12252  fprodssdc  12269  sinbnd  12431  cosbnd  12432  dvdscmulr  12499  dvdsmulcr  12500  oddm1even  12554  bitsmod  12635  bitsinv1lem  12640  qredeq  12786  cncongr2  12794  isprm3  12808  prmrp  12835  sqrt2irr  12852  crth  12914  pcdvdsb  13011  ssnnctlemct  13186  pwselbasb  13495  xpsfrnel2  13548  gsumval2  13599  imasmnd2  13654  grpid  13741  grpidrcan  13767  grpidlcan  13768  grplmulf1o  13776  imasgrp2  13816  ghmeqker  13977  abladdsub4  14020  imasrng  14089  imasring  14197  lspsnss2  14554  znf1o  14786  znidom  14792  znunit  14794  znrrg  14795  eltg3  14909  eltop  14921  eltop2  14922  eltop3  14923  lmbrf  15067  cncnpi  15080  txcn  15127  hmeoimaf1o  15166  ismet2  15206  xmseq0  15320  wilthlem1  15835  fsumdvdsmul  15846  lgsne0  15898  lgsquadlem1  15937  lgsquadlem2  15938  2sqlem7  15981  clwwlkn1  16400  eupth2lem2dc  16441  eupth2lem3lem3fi  16452  eupth2lem3lem6fi  16453