MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bitr3d Structured version   Unicode version

Theorem bitr3d 255
Description: Deduction form of bitr3i 251. (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
StepHypRef Expression
1 bitr3d.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21bicomd 201 . 2  |-  ( ph  ->  ( ch  <->  ps )
)
3 bitr3d.2 . 2  |-  ( ph  ->  ( ps  <->  th )
)
42, 3bitrd 253 1  |-  ( ph  ->  ( ch  <->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
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 185
This theorem is referenced by:  3bitrrd  280  3bitr3d  283  3bitr3rd  284  biass  359  sbequ12aOLD  1939  sbco2  2111  sbco2OLD  2112  sbco3  2114  sbco3OLD  2115  sb9iOLD  2128  sbcom2  2151  sbcom2OLD  2152  sbal1  2171  sbal1OLD  2172  sbal2  2173  sbal  2174  sbalOLD  2175  csbiebt  3303  prsspwg  4025  reusv2lem5  4492  copsex2t  4573  copsex2g  4574  ordtri2  4749  onmindif  4803  fnssresb  5518  fcnvres  5583  funimass5  5815  fmptco  5871  cbvfo  5988  isocnv  6016  isoini  6024  isoselem  6027  riota2df  6068  ovmpt2dxf  6211  caovcanrd  6261  onmindif2  6418  ordunisuc2  6450  dfom2  6473  ordge1n0  6930  ondif2  6934  oa00  6990  odi  7010  oeoe  7030  eceqoveq  7197  omsucdomOLD  7498  isfinite2  7562  unfilem1  7568  fodomfib  7583  inficl  7667  dffi3  7673  ordiso2  7721  ordtypelem9  7732  cantnfle  7871  cantnf  7893  cantnfleOLD  7901  cantnfOLD  7915  wemapwe  7920  wemapweOLD  7921  rankr1a  8035  bnd2  8092  iscard  8137  domtri2  8151  nnsdomel  8152  cardaleph  8251  dfac12lem2  8305  cfss  8426  axcc3  8599  fodomb  8685  iundom2g  8696  inar1  8934  ltpiord  9048  ordpinq  9104  suplem2pr  9214  enreceq  9228  subeq0  9627  negcon1  9653  subeqrev  9763  lesub  9810  ltsub13  9812  subge0  9844  mul0or  9968  mulcan1g  9981  div11  10012  divmuleq  10028  ltmuldiv2  10195  lemuldiv2  10204  nn1suc  10335  addltmul  10552  elnnnn0  10615  znn0sub  10684  prime  10714  uzindOLD  10728  zbtwnre  10943  xadddi2  11252  supxrbnd  11283  fz1n  11460  fzrev3  11514  fzonlt0  11564  modsubdir  11759  om2uzlt2i  11766  hashf1lem1  12200  cnpart  12721  sqr11  12744  sqrsq2  12750  absdiflt  12797  absdifle  12798  sqreulem  12839  sqreu  12840  eqsqror  12846  clim2  12974  climshft2  13052  isercoll  13137  sumrb  13182  supcvg  13310  sinbnd  13456  cosbnd  13457  sqr2irr  13523  dvdscmulr  13553  dvdsmulcr  13554  oddm1even  13585  bitsmod  13624  bitsinv1lem  13629  isprm3  13764  prmrp  13779  qredeq  13784  crt  13845  pcdvdsb  13927  pceq0  13929  unbenlem  13961  ramcl  14082  pwselbasb  14418  pwsle  14422  imasleval  14471  xpsfrnel2  14495  acsfn  14589  ismon2  14665  isepi2  14672  epii  14674  fthsect  14827  fthmon  14829  isipodrs  15323  ipodrsfi  15325  imasmnd2  15450  gsumval2a  15503  grpid  15564  grpidrcan  15582  grpidlcan  15583  grplmulf1o  15591  imasgrp2  15661  ghmeqker  15764  ghmf1  15766  gacan  15814  odmulgeq  16049  pgpssslw  16104  efgsfo  16227  efgred  16236  abladdsub4  16294  subgdmdprd  16521  imasrng  16701  lspsnss2  17066  gsumbagdiaglem  17425  znf1o  17964  znfld  17973  znunit  17976  znrrg  17978  iporthcom  18044  ip2eq  18062  obsne0  18130  lindfmm  18236  lindsmm  18237  lsslinds  18240  eltg3  18547  eltop  18559  eltop2  18560  eltop3  18561  lmbrf  18844  cncnpi  18862  dfcon2  19003  1stcfb  19029  elptr  19126  xkoccn  19172  txcn  19179  hausdiag  19198  hmeoimaf1o  19323  isfbas  19382  ufileu  19472  alexsubALTlem4  19602  tsmsf1o  19699  ismet2  19888  imasdsf1olem  19928  imasf1oxmet  19930  imasf1omet  19931  xmseq0  20019  imasf1oxms  20044  metucnOLD  20143  metucn  20144  nrmmetd  20147  nlmmul0or  20244  xrsxmet  20366  metdseq0  20410  elpi1i  20598  cphsqrcl2  20685  tchcph  20732  lmmbrf  20753  caucfil  20774  lmclim  20793  cmsss  20841  srabn  20852  ovolfioo  20931  ovolficc  20932  elovolmr  20939  ovolctb  20953  ovolicc2lem3  20982  mbfmulc2lem  21105  mbfimaopnlem  21113  itg2mulclem  21204  iblrelem  21248  ellimc2  21332  mdegle0  21528  fta1glem2  21618  dgreq0  21712  plydivlem4  21742  plydivex  21743  fta1  21754  quotcan  21755  logeftb  22012  quad2  22214  cubic2  22223  dquartlem1  22226  atandm4  22254  fsumharmonic  22385  wilthlem1  22386  basellem8  22405  mumullem2  22498  chpchtsum  22538  logfaclbnd  22541  dchrelbas4  22562  lgsne0  22652  lgsqrlem2  22661  lgsdchrval  22666  lgsquadlem1  22673  lgsquadlem2  22674  2sqlem7  22689  dchrisum0lem1  22745  trgcgrg  22947  tgcolg  22968  eupath2lem3  23568  grpoid  23678  grpodiveq  23711  nvsubadd  24003  nvmeq0  24012  nvgt0  24031  imsmetlem  24049  nmlnogt0  24165  ip2eqi  24225  hvaddcan2  24441  hvmulcan2  24443  hvaddsub4  24448  hi2eq  24475  pjhtheu  24765  lnopeqi  25380  riesz1  25437  jpi  25642  chcv2  25728  cvp  25747  atnemeq0  25749  fmptcof2  25947  funcnvmptOLD  25954  funcnvmpt  25955  nndiffz1  26043  nn0min  26058  xrge0addgt0  26122  lmlim  26346  eulerpartlems  26712  eulerpartlemgh  26730  ballotlemfc0  26844  ballotlemfcc  26845  sgnneg  26892  signsvfpn  26955  signsvfnn  26956  ghomf1olem  27282  fz0n  27358  prodrblem2  27413  imageval  27930  onsuct0  28257  onint1  28265  wl-sbcom2d  28356  wl-sbalnae  28357  wl-ax11-lem8  28379  wl-ax11-lem10  28381  sin2h  28393  tan2h  28395  heicant  28397  mblfinlem3  28401  ovoliunnfl  28404  voliunnfl  28406  volsupnfl  28407  mbfresfi  28409  mbfposadd  28410  dvtanlem  28412  itg2addnclem  28414  itg2addnclem2  28415  itg2addnc  28417  itg2gt0cn  28418  itgaddnclem2  28422  ftc1anclem5  28442  areacirclem1  28455  areacirclem4  28458  areacirc  28460  nn0prpwlem  28488  filnetlem4  28573  isdmn3  28845  rmxycomplete  29229  gicabl  29425  pm14.123b  29651  iotavalb  29655  climreeq  29757  frgra3vlem2  30564  ovmpt2rdxf  30699  bnj1280  31940  bj-flbi3  32427  bj-msub  32488  bj-mdiv  32491  lcvp  32578  lcv2  32580  lsatnem0  32583  atnem0  32856  cvlsupr2  32881  cvr2N  32948  athgt  32993  2llnmat  33061  pmap11  33299  pmapeq0  33303  2lnat  33321  paddclN  33379  pmapjat1  33390  ltrn2ateq  33717  dihcnvord  34812  dihcnv11  34813  dih0bN  34819  dih0sb  34823  dihlspsnat  34871  dihatexv2  34877  dihglblem6  34878  dochvalr  34895  dochn0nv  34913  djhcvat42  34953  dochsatshp  34989  dochshpsat  34992  dochkrsat2  34994  lcfl5a  35035  lcfl8a  35041  lclkrlem2a  35045  mapdcnvordN  35196  hdmap14lem4a  35412  hgmapeq0  35445  hdmaplkr  35454  hdmapellkr  35455
  Copyright terms: Public domain W3C validator