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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  3bitrrd  215  3bitr3d  218  3bitr3rd  219  pm5.16  840  biassdc  1444  pm5.24dc  1447  anxordi  1449  sbequ12a  1826  drex1  1851  sbcomxyyz  2032  sb9v  2038  csbiebt  3187  prsspwg  3875  ssprss  3876  bnd2  4312  copsex2t  4387  copsex2g  4388  fnssresb  5498  fcnvres  5578  foelcdmi  5758  dmfco  5776  funimass5  5829  fmptco  5877  cbvfo  5994  cbvexfo  5995  isocnv  6020  isoini  6027  isoselem  6029  riota2df  6063  ovmpodxf  6217  caovcanrd  6256  suppimacnvfn  6490  fidcenumlemrks  7276  ordiso2  7382  ltpiord  7693  dfplpq2  7728  dfmpq2  7729  enqeceq  7733  enq0eceq  7811  enreceq  8110  ltpsrprg  8177  mappsrprg  8178  cnegexlem3  8511  subeq0  8560  negcon1  8586  subexsub  8706  subeqrev  8710  lesub  8777  ltsub13  8779  subge0  8811  div11ap  9039  divmuleqap  9056  ltmuldiv2  9214  lemuldiv2  9221  nn1suc  9333  addltmul  9554  elnnnn0  9618  znn0sub  9722  prime  9757  indstr  10010  qapne  10056  qlttri2  10058  fz1n  10466  fzrev3  10512  fzo0n  10593  fzonlt0  10594  divfl0  10753  modqsubdir  10852  fzfig  10889  hashf1lem1  11308  wrdlenge1n0  11361  pfxccat3a  11533  sqrt11  11828  sqrtsq2  11832  absdiflt  11882  absdifle  11883  nnabscl  11890  minclpr  12028  xrnegiso  12054  xrnegcon1d  12056  clim2  12075  climshft2  12098  sumrbdc  12172  prodrbdclem2  12366  fprodssdc  12383  sinbnd  12545  cosbnd  12546  dvdscmulr  12613  dvdsmulcr  12614  oddm1even  12668  bitsmod  12749  bitsinv1lem  12754  qredeq  12900  cncongr2  12908  isprm3  12922  prmrp  12950  sqrt2irr  12967  crth  13032  pcdvdsb  13129  ballotfilemfc0  13291  ballotfilemfcc  13292  ssnnctlemct  13396  xpsfrnel2  13727  gzsumval2  13774  imasmnd2  13819  grpid  13904  grpidrcan  13930  grpidlcan  13931  grplmulf1o  13939  imasgrp2  13973  ghmeqker  14134  abladdsub4  14209  pwselbasb  14314  imasrng  14363  imasring  14479  lspsnss2  14866  znf1o  15096  znidom  15102  znunit  15104  znrrg  15105  gsumbagdiaglem  15180  eltg3  15295  eltop  15307  eltop2  15308  eltop3  15309  lmbrf  15453  cncnpi  15466  txcn  15513  hmeoimaf1o  15552  ismet2  15592  xmseq0  15706  wilthlem1  16244  fsumdvdsmul  16297  lgsne0  16374  lgsquadlem1  16413  lgsquadlem2  16414  2sqlem7  16457  clwwlkn1  16876  eupth2lem2dc  16917  eupth2lem3lem3fi  16928  eupth2lem3lem6fi  16929