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  4310  copsex2t  4385  copsex2g  4386  fnssresb  5495  fcnvres  5575  foelcdmi  5755  dmfco  5773  funimass5  5826  fmptco  5874  cbvfo  5991  cbvexfo  5992  isocnv  6017  isoini  6024  isoselem  6026  riota2df  6060  ovmpodxf  6214  caovcanrd  6253  suppimacnvfn  6486  fidcenumlemrks  7270  ordiso2  7375  ltpiord  7686  dfplpq2  7721  dfmpq2  7722  enqeceq  7726  enq0eceq  7804  enreceq  8103  ltpsrprg  8170  mappsrprg  8171  cnegexlem3  8504  subeq0  8553  negcon1  8579  subexsub  8699  subeqrev  8703  lesub  8770  ltsub13  8772  subge0  8804  div11ap  9032  divmuleqap  9049  ltmuldiv2  9207  lemuldiv2  9214  nn1suc  9325  addltmul  9546  elnnnn0  9610  znn0sub  9714  prime  9749  indstr  10002  qapne  10048  qlttri2  10050  fz1n  10458  fzrev3  10504  fzo0n  10585  fzonlt0  10586  divfl0  10744  modqsubdir  10843  fzfig  10880  hashf1lem1  11299  wrdlenge1n0  11352  pfxccat3a  11524  sqrt11  11819  sqrtsq2  11823  absdiflt  11873  absdifle  11874  nnabscl  11881  minclpr  12018  xrnegiso  12044  xrnegcon1d  12046  clim2  12065  climshft2  12088  sumrbdc  12162  prodrbdclem2  12356  fprodssdc  12373  sinbnd  12535  cosbnd  12536  dvdscmulr  12603  dvdsmulcr  12604  oddm1even  12658  bitsmod  12739  bitsinv1lem  12744  qredeq  12890  cncongr2  12898  isprm3  12912  prmrp  12940  sqrt2irr  12957  crth  13022  pcdvdsb  13119  ballotfilemfc0  13281  ballotfilemfcc  13282  ssnnctlemct  13386  xpsfrnel2  13716  gzsumval2  13763  imasmnd2  13808  grpid  13893  grpidrcan  13919  grpidlcan  13920  grplmulf1o  13928  imasgrp2  13962  ghmeqker  14123  abladdsub4  14167  pwselbasb  14255  imasrng  14304  imasring  14418  lspsnss2  14805  znf1o  15035  znidom  15041  znunit  15043  znrrg  15044  eltg3  15207  eltop  15219  eltop2  15220  eltop3  15221  lmbrf  15365  cncnpi  15378  txcn  15425  hmeoimaf1o  15464  ismet2  15504  xmseq0  15618  wilthlem1  16151  fsumdvdsmul  16204  lgsne0  16276  lgsquadlem1  16315  lgsquadlem2  16316  2sqlem7  16359  clwwlkn1  16778  eupth2lem2dc  16819  eupth2lem3lem3fi  16830  eupth2lem3lem6fi  16831