Theorem bitr3d 270

Description: Deduction form of bitr3i 266. (Contributed by NM, 14-May-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 213	. 2 |- ( ph -> ( ch <-> ps ) )
3		bitr3d.2	. 2 |- ( ph -> ( ps <-> th ) )
4	2, 3	bitrd 268	1 |- ( ph -> ( ch <-> th ) )

Syntax hints:   -> wi 4   <-> wb 196

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197

This theorem is referenced by:  3bitrrd  295  3bitr3d  298  3bitr3rd  299  biass  374  19.21t  2073  sbco2  2415  sbco3  2417  sbcom2  2445  sbal1  2460  sbal2  2461  sbal  2462  csbiebt  3553  prsspwg  4355  ssprss  4356  reusv2lem5  4873  copsex2t  4957  copsex2g  4958  ordtri2  5758  onmindif  5815  fnssresb  6003  fcnvres  6082  foelrni  6244  funimass5  6334  fmptco  6396  cbvfo  6544  isocnv  6580  isoini  6588  isoselem  6591  riota2df  6631  ovmpt2dxf  6786  caovcanrd  6837  onmindif2  7012  ordunisuc2  7044  dfom2  7067  ordge1n0  7578  ondif2  7582  oa00  7639  odi  7659  oeoe  7679  eceqoveq  7853  isfinite2  8218  unfilem1  8224  fodomfib  8240  inficl  8331  dffi3  8337  ordiso2  8420  ordtypelem9  8431  cantnfle  8568  cantnf  8590  wemapwe  8594  rankr1a  8699  bnd2  8756  iscard  8801  domtri2  8815  nnsdomel  8816  cardaleph  8912  dfac12lem2  8966  cfss  9087  axcc3  9260  fodomb  9348  iundom2g  9362  inar1  9597  ltpiord  9709  ordpinq  9765  suplem2pr  9875  enreceq  9887  subeq0  10307  negcon1  10333  subexsub  10449  subeqrev  10453  lesub  10507  ltsub13  10509  subge0  10541  mul0or  10667  mulcan1g  10680  div11  10713  divmuleq  10730  ltmuldiv2  10897  lemuldiv2  10904  nn1suc  11041  addltmul  11268  elnnnn0  11336  znn0sub  11424  prime  11458  zbtwnre  11786  xadddi2  12127  supxrbnd  12158  fz1n  12359  fzrev3  12406  fzo0n  12490  fzonlt0  12491  ico01fl0  12620  modsubdir  12739  om2uzlt2i  12750  hashf1lem1  13239  wrdlenge1n0  13340  cnpart  13980  sqrt11  14003  sqrtsq2  14009  absdiflt  14057  absdifle  14058  sqreulem  14099  sqreu  14100  eqsqrtor  14106  clim2  14235  climshft2  14313  isercoll  14398  sumrb  14444  supcvg  14588  prodrblem2  14661  sinbnd  14910  cosbnd  14911  sqrt2irr  14979  dvdscmulr  15010  dvdsmulcr  15011  oddm1even  15067  bitsmod  15158  bitsinv1lem  15163  qredeq  15371  cncongr2  15382  isprm3  15396  prmrp  15424  crth  15483  pcdvdsb  15573  pceq0  15575  unbenlem  15612  ramcl  15733  pwselbasb  16148  pwsle  16152  imasleval  16201  xpsfrnel2  16225  acsfn  16320  ismon2  16394  isepi2  16401  epii  16403  fthsect  16585  fthmon  16587  isipodrs  17161  ipodrsfi  17163  gsumval2a  17279  imasmnd2  17327  grpid  17457  grpidrcan  17480  grpidlcan  17481  grplmulf1o  17489  imasgrp2  17530  ghmeqker  17687  ghmf1  17689  gacan  17738  odmulgeq  17974  pgpssslw  18029  efgsfo  18152  efgred  18161  abladdsub4  18219  subgdmdprd  18433  imasring  18619  lspsnss2  19005  0ring01eqbi  19273  gsumbagdiaglem  19375  znf1o  19900  znfld  19909  znunit  19912  znrrg  19914  iporthcom  19980  ip2eq  19998  obsne0  20069  lindfmm  20166  lindsmm  20167  lsslinds  20170  eltg3  20766  eltop  20778  eltop2  20779  eltop3  20780  lmbrf  21064  cncnpi  21082  dfconn2  21222  1stcfb  21248  elptr  21376  xkoccn  21422  txcn  21429  hausdiag  21448  hmeoimaf1o  21573  isfbas  21633  ufileu  21723  alexsubALTlem4  21854  tsmsf1o  21948  ismet2  22138  imasdsf1olem  22178  imasf1oxmet  22180  imasf1omet  22181  xmseq0  22269  imasf1oxms  22294  metucn  22376  nrmmetd  22379  nmgt0  22434  nlmmul0or  22487  xrsxmet  22612  metdseq0  22657  elpi1i  22846  cphsqrtcl2  22986  tchcph  23036  lmmbrf  23060  caucfil  23081  lmclim  23101  cmsss  23147  srabn  23156  ovolfioo  23236  ovolficc  23237  elovolmr  23244  ovolctb  23258  ovolicc2lem3  23287  mbfmulc2lem  23414  mbfimaopnlem  23422  itg2mulclem  23513  iblrelem  23557  ellimc2  23641  mdegle0  23837  fta1glem2  23926  dgreq0  24021  plydivlem4  24051  plydivex  24052  fta1  24063  quotcan  24064  logeftb  24330  quad2  24566  cubic2  24575  dquartlem1  24578  atandm4  24606  fsumharmonic  24738  wilthlem1  24794  basellem8  24814  mumullem2  24906  chpchtsum  24944  logfaclbnd  24947  dchrelbas4  24968  lgsne0  25060  lgsqrlem2  25072  lgsdchrval  25079  lgsquadlem1  25105  lgsquadlem2  25106  2sqlem7  25149  dchrisum0lem1  25205  trgcgrg  25410  tgcgr4  25426  tgcolg  25449  lmiinv  25684  iseqlg  25747  cusgruvtxb  26318  eupth2lem3lem3  27090  eupth2lem3lem6  27093  frgr3vlem2  27138  grpoid  27374  nvmeq0  27513  nvgt0  27529  imsmetlem  27545  nmlnogt0  27652  ip2eqi  27712  hvaddcan2  27928  hvmulcan2  27930  hvaddsub4  27935  hi2eq  27962  pjhtheu  28253  lnopeqi  28867  riesz1  28924  jpi  29129  chcv2  29215  cvp  29234  atnemeq0  29236  brabgaf  29420  fmptcof2  29457  funcnvmptOLD  29467  funcnvmpt  29468  nndiffz1  29548  nn0min  29567  xrge0addgt0  29691  smatrcl  29862  lmlim  29993  carsggect  30380  eulerpartlems  30422  eulerpartlemgh  30440  ballotlemfc0  30554  ballotlemfcc  30555  sgnneg  30602  signsvfpn  30662  signsvfnn  30663  reprdifc  30705  bnj1280  31088  elmrsubrn  31417  msubff1  31453  fz0n  31616  slenlt  31877  imageval  32037  nn0prpwlem  32317  filnetlem4  32376  onsuct0  32440  onint1  32448  bj-mdiv  33157  dissneqlem  33187  wl-sbalnae  33345  wl-ax11-lem8  33369  wl-ax11-lem10  33371  sin2h  33399  tan2h  33401  matunitlindflem1  33405  matunitlindflem2  33406  matunitlindf  33407  poimirlem18  33427  poimirlem21  33430  poimirlem24  33433  heicant  33444  mblfinlem3  33448  ovoliunnfl  33451  voliunnfl  33453  volsupnfl  33454  mbfresfi  33456  mbfposadd  33457  itg2addnclem  33461  itg2addnclem2  33462  itg2addnc  33464  itg2gt0cn  33465  itgaddnclem2  33469  ftc1anclem5  33489  areacirclem1  33500  areacirclem4  33503  areacirc  33505  isdmn3  33873  eldmres2  34038  lcvp  34327  lcv2  34329  lsatnem0  34332  atnem0  34605  cvlsupr2  34630  cvr2N  34697  athgt  34742  2llnmat  34810  pmap11  35048  pmapeq0  35052  2lnat  35070  paddclN  35128  pmapjat1  35139  ltrn2ateq  35467  dihcnvord  36563  dihcnv11  36564  dih0bN  36570  dih0sb  36574  dihlspsnat  36622  dihatexv2  36628  dihglblem6  36629  dochvalr  36646  dochn0nv  36664  djhcvat42  36704  dochsatshp  36740  dochshpsat  36743  dochkrsat2  36745  lcfl5a  36786  lcfl8a  36792  lclkrlem2a  36796  mapdcnvordN  36947  hdmap14lem4a  37163  hgmapeq0  37196  hdmaplkr  37205  hdmapellkr  37206  rmxycomplete  37482  gicabl  37669  ntrneiel  38379  ntrneik4w  38398  ntrneik4  38399  extoimad  38464  radcnvrat  38513  pm14.123b  38627  iotavalb  38631  infxrunb3  39651  climreeq  39845  clim2f  39868  clim2f2  39902  pfxccat3a  41429  dfodd4  41571  oddprmne2  41624  nnsgrpnmnd  41818  ovmpt2rdxf  42117