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, 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
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  1938  sbco2  2112  sbco2OLD  2113  sbco3  2115  sbco3OLD  2116  sbcomOLD  2118  sb9iOLD  2130  sbcom2  2153  sbcom2OLD  2154  sbal1  2173  sbal1OLD  2174  sbal2  2175  sbal  2176  sbalOLD  2177  csbiebt  3296  prsspwg  4018  reusv2lem5  4485  copsex2t  4566  copsex2g  4567  ordtri2  4741  onmindif  4795  fnssresb  5511  fcnvres  5576  funimass5  5808  fmptco  5863  cbvfo  5980  isocnv  6008  isoini  6016  isoselem  6019  riota2df  6061  ovmpt2dxf  6205  caovcanrd  6255  onmindif2  6412  ordunisuc2  6444  dfom2  6467  ordge1n0  6926  ondif2  6930  oa00  6986  odi  7006  oeoe  7026  eceqoveq  7193  omsucdomOLD  7494  isfinite2  7558  unfilem1  7564  fodomfib  7579  inficl  7663  dffi3  7669  ordiso2  7717  ordtypelem9  7728  cantnfle  7867  cantnf  7889  cantnfleOLD  7897  cantnfOLD  7911  wemapwe  7916  wemapweOLD  7917  rankr1a  8031  bnd2  8088  iscard  8133  domtri2  8147  nnsdomel  8148  cardaleph  8247  dfac12lem2  8301  cfss  8422  axcc3  8595  fodomb  8681  iundom2g  8692  inar1  8930  ltpiord  9044  ordpinq  9100  suplem2pr  9210  enreceq  9224  subeq0  9623  negcon1  9649  subeqrev  9759  lesub  9806  ltsub13  9808  subge0  9840  mul0or  9964  mulcan1g  9977  div11  10008  divmuleq  10024  ltmuldiv2  10191  lemuldiv2  10200  nn1suc  10331  addltmul  10548  elnnnn0  10611  znn0sub  10680  prime  10710  uzindOLD  10724  zbtwnre  10939  xadddi2  11248  supxrbnd  11279  fz1n  11455  fzrev3  11506  fzonlt0  11556  modsubdir  11751  om2uzlt2i  11758  hashf1lem1  12192  cnpart  12713  sqr11  12736  sqrsq2  12742  absdiflt  12789  absdifle  12790  sqreulem  12831  sqreu  12832  eqsqror  12838  clim2  12966  climshft2  13044  isercoll  13129  sumrb  13174  supcvg  13301  sinbnd  13447  cosbnd  13448  sqr2irr  13514  dvdscmulr  13544  dvdsmulcr  13545  oddm1even  13576  bitsmod  13615  bitsinv1lem  13620  isprm3  13755  prmrp  13770  qredeq  13775  crt  13836  pcdvdsb  13918  pceq0  13920  unbenlem  13952  ramcl  14073  pwselbasb  14409  pwsle  14413  imasleval  14462  xpsfrnel2  14486  acsfn  14580  ismon2  14656  isepi2  14663  epii  14665  fthsect  14818  fthmon  14820  isipodrs  15314  ipodrsfi  15316  imasmnd2  15441  gsumval2a  15492  grpid  15553  grpidrcan  15571  grpidlcan  15572  grplmulf1o  15580  imasgrp2  15650  ghmeqker  15753  ghmf1  15755  gacan  15803  odmulgeq  16038  pgpssslw  16093  efgsfo  16216  efgred  16225  abladdsub4  16283  subgdmdprd  16505  imasrng  16646  lspsnss2  17008  gsumbagdiaglem  17379  znf1o  17826  znfld  17835  znunit  17838  znrrg  17840  iporthcom  17906  ip2eq  17924  obsne0  17992  lindfmm  18098  lindsmm  18099  lsslinds  18102  eltg3  18409  eltop  18421  eltop2  18422  eltop3  18423  lmbrf  18706  cncnpi  18724  dfcon2  18865  1stcfb  18891  elptr  18988  xkoccn  19034  txcn  19041  hausdiag  19060  hmeoimaf1o  19185  isfbas  19244  ufileu  19334  alexsubALTlem4  19464  tsmsf1o  19561  ismet2  19750  imasdsf1olem  19790  imasf1oxmet  19792  imasf1omet  19793  xmseq0  19881  imasf1oxms  19906  metucnOLD  20005  metucn  20006  nrmmetd  20009  nlmmul0or  20106  xrsxmet  20228  metdseq0  20272  elpi1i  20460  cphsqrcl2  20547  tchcph  20594  lmmbrf  20615  caucfil  20636  lmclim  20655  cmsss  20703  srabn  20714  ovolfioo  20793  ovolficc  20794  elovolmr  20801  ovolctb  20815  ovolicc2lem3  20844  mbfmulc2lem  20967  mbfimaopnlem  20975  itg2mulclem  21066  iblrelem  21110  ellimc2  21194  mdegle0  21433  fta1glem2  21523  dgreq0  21617  plydivlem4  21647  plydivex  21648  fta1  21659  quotcan  21660  logeftb  21917  quad2  22119  cubic2  22128  dquartlem1  22131  atandm4  22159  fsumharmonic  22290  wilthlem1  22291  basellem8  22310  mumullem2  22403  chpchtsum  22443  logfaclbnd  22446  dchrelbas4  22467  lgsne0  22557  lgsqrlem2  22566  lgsdchrval  22571  lgsquadlem1  22578  lgsquadlem2  22579  2sqlem7  22594  dchrisum0lem1  22650  trgcgrg  22848  tgcolg  22867  eupath2lem3  23423  grpoid  23533  grpodiveq  23566  nvsubadd  23858  nvmeq0  23867  nvgt0  23886  imsmetlem  23904  nmlnogt0  24020  ip2eqi  24080  hvaddcan2  24296  hvmulcan2  24298  hvaddsub4  24303  hi2eq  24330  pjhtheu  24620  lnopeqi  25235  riesz1  25292  jpi  25497  chcv2  25583  cvp  25602  atnemeq0  25604  fmptcof2  25803  funcnvmptOLD  25810  funcnvmpt  25811  nndiffz1  25898  nn0min  25913  xrge0addgt0  25977  lmlim  26231  eulerpartlems  26591  eulerpartlemgh  26609  ballotlemfc0  26723  ballotlemfcc  26724  sgnneg  26771  signsvfpn  26834  signsvfnn  26835  ghomf1olem  27160  fz0n  27236  prodrblem2  27291  imageval  27808  onsuct0  28135  onint1  28143  wl-sbcom2d  28235  wl-sbalnae  28236  wl-ax11-lem8  28252  wl-ax11-lem10  28254  sin2h  28266  tan2h  28268  heicant  28270  mblfinlem3  28274  ovoliunnfl  28277  voliunnfl  28279  volsupnfl  28280  mbfresfi  28282  mbfposadd  28283  dvtanlem  28285  itg2addnclem  28287  itg2addnclem2  28288  itg2addnc  28290  itg2gt0cn  28291  itgaddnclem2  28295  ftc1anclem5  28315  areacirclem1  28328  areacirclem4  28331  areacirc  28333  nn0prpwlem  28361  filnetlem4  28446  isdmn3  28718  rmxycomplete  29103  gicabl  29299  pm14.123b  29525  iotavalb  29529  climreeq  29632  frgra3vlem2  30439  ovmpt2rdxf  30573  bnj1280  31713  bj-flbi3  32107  bj-msub  32168  bj-mdiv  32171  lcvp  32258  lcv2  32260  lsatnem0  32263  atnem0  32536  cvlsupr2  32561  cvr2N  32628  athgt  32673  2llnmat  32741  pmap11  32979  pmapeq0  32983  2lnat  33001  paddclN  33059  pmapjat1  33070  ltrn2ateq  33397  dihcnvord  34492  dihcnv11  34493  dih0bN  34499  dih0sb  34503  dihlspsnat  34551  dihatexv2  34557  dihglblem6  34558  dochvalr  34575  dochn0nv  34593  djhcvat42  34633  dochsatshp  34669  dochshpsat  34672  dochkrsat2  34674  lcfl5a  34715  lcfl8a  34721  lclkrlem2a  34725  mapdcnvordN  34876  hdmap14lem4a  35092  hgmapeq0  35125  hdmaplkr  35134  hdmapellkr  35135
  Copyright terms: Public domain W3C validator