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  1787  drex1  1812  sbcomxyyz  1991  sb9v  1997  csbiebt  3124  prsspwg  3783  bnd2  4207  copsex2t  4279  copsex2g  4280  fnssresb  5373  fcnvres  5444  foelcdmi  5616  dmfco  5632  funimass5  5682  fmptco  5731  cbvfo  5835  cbvexfo  5836  isocnv  5861  isoini  5868  isoselem  5870  riota2df  5901  ovmpodxf  6052  caovcanrd  6091  fidcenumlemrks  7028  ordiso2  7110  ltpiord  7405  dfplpq2  7440  dfmpq2  7441  enqeceq  7445  enq0eceq  7523  enreceq  7822  ltpsrprg  7889  mappsrprg  7890  cnegexlem3  8222  subeq0  8271  negcon1  8297  subexsub  8417  subeqrev  8421  lesub  8487  ltsub13  8489  subge0  8521  div11ap  8746  divmuleqap  8763  ltmuldiv2  8921  lemuldiv2  8928  nn1suc  9028  addltmul  9247  elnnnn0  9311  znn0sub  9410  prime  9444  indstr  9686  qapne  9732  qlttri2  9734  fz1n  10138  fzrev3  10181  fzonlt0  10262  divfl0  10405  modqsubdir  10504  fzfig  10541  wrdlenge1n0  10987  sqrt11  11223  sqrtsq2  11227  absdiflt  11276  absdifle  11277  nnabscl  11284  minclpr  11421  xrnegiso  11446  xrnegcon1d  11448  clim2  11467  climshft2  11490  sumrbdc  11563  prodrbdclem2  11757  fprodssdc  11774  sinbnd  11936  cosbnd  11937  dvdscmulr  12004  dvdsmulcr  12005  oddm1even  12059  bitsmod  12140  bitsinv1lem  12145  qredeq  12291  cncongr2  12299  isprm3  12313  prmrp  12340  sqrt2irr  12357  crth  12419  pcdvdsb  12516  ssnnctlemct  12690  pwselbasb  12997  xpsfrnel2  13050  gsumval2  13101  imasmnd2  13156  grpid  13243  grpidrcan  13269  grpidlcan  13270  grplmulf1o  13278  imasgrp2  13318  ghmeqker  13479  abladdsub4  13522  imasrng  13590  imasring  13698  lspsnss2  14053  znf1o  14285  znidom  14291  znunit  14293  znrrg  14294  eltg3  14379  eltop  14391  eltop2  14392  eltop3  14393  lmbrf  14537  cncnpi  14550  txcn  14597  hmeoimaf1o  14636  ismet2  14676  xmseq0  14790  wilthlem1  15302  fsumdvdsmul  15313  lgsne0  15365  lgsquadlem1  15404  lgsquadlem2  15405  2sqlem7  15448