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  828  biassdc  1395  pm5.24dc  1398  anxordi  1400  sbequ12a  1773  drex1  1798  sbcomxyyz  1972  sb9v  1978  csbiebt  3096  prsspwg  3752  bnd2  4173  copsex2t  4245  copsex2g  4246  fnssresb  5328  fcnvres  5399  foelcdmi  5568  dmfco  5584  funimass5  5633  fmptco  5682  cbvfo  5785  cbvexfo  5786  isocnv  5811  isoini  5818  isoselem  5820  riota2df  5850  ovmpodxf  5999  caovcanrd  6037  fidcenumlemrks  6951  ordiso2  7033  ltpiord  7317  dfplpq2  7352  dfmpq2  7353  enqeceq  7357  enq0eceq  7435  enreceq  7734  ltpsrprg  7801  mappsrprg  7802  cnegexlem3  8133  subeq0  8182  negcon1  8208  subexsub  8328  subeqrev  8332  lesub  8397  ltsub13  8399  subge0  8431  div11ap  8656  divmuleqap  8673  ltmuldiv2  8831  lemuldiv2  8838  nn1suc  8937  addltmul  9154  elnnnn0  9218  znn0sub  9317  prime  9351  indstr  9592  qapne  9638  qlttri2  9640  fz1n  10043  fzrev3  10086  fzonlt0  10166  divfl0  10295  modqsubdir  10392  fzfig  10429  sqrt11  11047  sqrtsq2  11051  absdiflt  11100  absdifle  11101  nnabscl  11108  minclpr  11244  xrnegiso  11269  xrnegcon1d  11271  clim2  11290  climshft2  11313  sumrbdc  11386  prodrbdclem2  11580  fprodssdc  11597  sinbnd  11759  cosbnd  11760  dvdscmulr  11826  dvdsmulcr  11827  oddm1even  11879  qredeq  12095  cncongr2  12103  isprm3  12117  prmrp  12144  sqrt2irr  12161  crth  12223  pcdvdsb  12318  ssnnctlemct  12446  xpsfrnel2  12764  grpid  12911  grpidrcan  12934  grpidlcan  12935  grplmulf1o  12943  abladdsub4  13115  eltg3  13527  eltop  13539  eltop2  13540  eltop3  13541  lmbrf  13685  cncnpi  13698  txcn  13745  hmeoimaf1o  13784  ismet2  13824  xmseq0  13938  lgsne0  14409  2sqlem7  14438