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  1981  sbco2  2144  sbco3  2146  sbcom2  2175  sbal1  2190  sbal2  2191  sbal  2192  csbiebt  3440  prsspwg  4172  reusv2lem5  4642  copsex2t  4724  copsex2g  4725  ordtri2  4903  onmindif  4957  fnssresb  5683  fcnvres  5752  foelrni  5906  funimass5  5989  fmptco  6049  cbvfo  6177  isocnv  6211  isoini  6219  isoselem  6222  riota2df  6263  ovmpt2dxf  6413  caovcanrd  6463  onmindif2  6632  ordunisuc2  6664  dfom2  6687  ordge1n0  7150  ondif2  7154  oa00  7210  odi  7230  oeoe  7250  eceqoveq  7418  omsucdomOLD  7715  isfinite2  7780  unfilem1  7786  fodomfib  7802  inficl  7887  dffi3  7893  ordiso2  7943  ordtypelem9  7954  cantnfle  8093  cantnf  8115  cantnfleOLD  8123  cantnfOLD  8137  wemapwe  8142  wemapweOLD  8143  rankr1a  8257  bnd2  8314  iscard  8359  domtri2  8373  nnsdomel  8374  cardaleph  8473  dfac12lem2  8527  cfss  8648  axcc3  8821  fodomb  8907  iundom2g  8918  inar1  9156  ltpiord  9268  ordpinq  9324  suplem2pr  9434  enreceq  9446  subeq0  9850  negcon1  9876  subeqrev  9988  lesub  10037  ltsub13  10039  subge0  10071  mul0or  10195  mulcan1g  10208  div11  10239  divmuleq  10255  ltmuldiv2  10422  lemuldiv2  10431  nn1suc  10563  addltmul  10780  elnnnn0  10845  znn0sub  10917  prime  10949  uzindOLD  10963  zbtwnre  11189  xadddi2  11498  supxrbnd  11529  fz1n  11713  fzrev3  11754  fzonlt0  11827  modsubdir  12034  om2uzlt2i  12041  hashf1lem1  12483  wrdlenge1n0  12555  cnpart  13052  sqrt11  13075  sqrtsq2  13081  absdiflt  13129  absdifle  13130  sqreulem  13171  sqreu  13172  eqsqrtor  13178  clim2  13306  climshft2  13384  isercoll  13469  sumrb  13514  supcvg  13646  sinbnd  13792  cosbnd  13793  sqrt2irr  13859  dvdscmulr  13889  dvdsmulcr  13890  oddm1even  13924  bitsmod  13963  bitsinv1lem  13968  isprm3  14103  prmrp  14119  qredeq  14124  crt  14185  pcdvdsb  14269  pceq0  14271  unbenlem  14303  ramcl  14424  pwselbasb  14762  pwsle  14766  imasleval  14815  xpsfrnel2  14839  acsfn  14933  ismon2  15006  isepi2  15013  epii  15015  fthsect  15168  fthmon  15170  isipodrs  15665  ipodrsfi  15667  gsumval2a  15780  imasmnd2  15831  grpid  15959  grpidrcan  15977  grpidlcan  15978  grplmulf1o  15986  imasgrp2  16059  ghmeqker  16167  ghmf1  16169  gacan  16217  odmulgeq  16453  pgpssslw  16508  efgsfo  16631  efgred  16640  abladdsub4  16698  subgdmdprd  16955  imasring  17142  lspsnss2  17525  0ring01eqbi  17795  gsumbagdiaglem  17901  znf1o  18463  znfld  18472  znunit  18475  znrrg  18477  iporthcom  18543  ip2eq  18561  obsne0  18629  lindfmm  18735  lindsmm  18736  lsslinds  18739  eltg3  19336  eltop  19349  eltop2  19350  eltop3  19351  lmbrf  19634  cncnpi  19652  dfcon2  19793  1stcfb  19819  elptr  19947  xkoccn  19993  txcn  20000  hausdiag  20019  hmeoimaf1o  20144  isfbas  20203  ufileu  20293  alexsubALTlem4  20423  tsmsf1o  20520  ismet2  20709  imasdsf1olem  20749  imasf1oxmet  20751  imasf1omet  20752  xmseq0  20840  imasf1oxms  20865  metucnOLD  20964  metucn  20965  nrmmetd  20968  nlmmul0or  21065  xrsxmet  21187  metdseq0  21231  elpi1i  21419  cphsqrtcl2  21506  tchcph  21553  lmmbrf  21574  caucfil  21595  lmclim  21614  cmsss  21662  srabn  21673  ovolfioo  21752  ovolficc  21753  elovolmr  21760  ovolctb  21774  ovolicc2lem3  21803  mbfmulc2lem  21927  mbfimaopnlem  21935  itg2mulclem  22026  iblrelem  22070  ellimc2  22154  mdegle0  22350  fta1glem2  22440  dgreq0  22534  plydivlem4  22564  plydivex  22565  fta1  22576  quotcan  22577  logeftb  22840  quad2  23042  cubic2  23051  dquartlem1  23054  atandm4  23082  fsumharmonic  23213  wilthlem1  23214  basellem8  23233  mumullem2  23326  chpchtsum  23366  logfaclbnd  23369  dchrelbas4  23390  lgsne0  23480  lgsqrlem2  23489  lgsdchrval  23494  lgsquadlem1  23501  lgsquadlem2  23502  2sqlem7  23517  dchrisum0lem1  23573  trgcgrg  23778  tgcolg  23813  lmiinv  24030  eupath2lem3  24851  frgra3vlem2  24873  grpoid  25097  grpodiveq  25130  nvsubadd  25422  nvmeq0  25431  nvgt0  25450  imsmetlem  25468  nmlnogt0  25584  ip2eqi  25644  hvaddcan2  25860  hvmulcan2  25862  hvaddsub4  25867  hi2eq  25894  pjhtheu  26184  lnopeqi  26799  riesz1  26856  jpi  27061  chcv2  27147  cvp  27166  atnemeq0  27168  fmptcof2  27374  funcnvmptOLD  27381  funcnvmpt  27382  nndiffz1  27468  nn0min  27484  xrge0addgt0  27554  lmlim  27802  eulerpartlems  28172  eulerpartlemgh  28190  ballotlemfc0  28304  ballotlemfcc  28305  sgnneg  28352  signsvfpn  28415  signsvfnn  28416  elmrsubrn  28753  msubff1  28789  ghomf1olem  28907  fz0n  28983  prodrblem2  29038  imageval  29555  onsuct0  29881  onint1  29889  wl-sbalnae  29987  wl-ax11-lem8  30007  wl-ax11-lem10  30009  sin2h  30020  tan2h  30022  heicant  30024  mblfinlem3  30028  ovoliunnfl  30031  voliunnfl  30033  volsupnfl  30034  mbfresfi  30036  mbfposadd  30037  dvtanlem  30039  itg2addnclem  30041  itg2addnclem2  30042  itg2addnc  30044  itg2gt0cn  30045  itgaddnclem2  30049  ftc1anclem5  30069  areacirclem1  30082  areacirclem4  30085  areacirc  30087  nn0prpwlem  30115  filnetlem4  30174  isdmn3  30446  rmxycomplete  30828  gicabl  31022  radcnvrat  31171  pm14.123b  31287  iotavalb  31291  climreeq  31527  clim2f  31550  nnsgrpnmnd  32343  ovmpt2rdxf  32661  bnj1280  33809  bj-flbi3  34348  bj-msub  34413  bj-mdiv  34416  lcvp  34505  lcv2  34507  lsatnem0  34510  atnem0  34783  cvlsupr2  34808  cvr2N  34875  athgt  34920  2llnmat  34988  pmap11  35226  pmapeq0  35230  2lnat  35248  paddclN  35306  pmapjat1  35317  ltrn2ateq  35645  dihcnvord  36741  dihcnv11  36742  dih0bN  36748  dih0sb  36752  dihlspsnat  36800  dihatexv2  36806  dihglblem6  36807  dochvalr  36824  dochn0nv  36842  djhcvat42  36882  dochsatshp  36918  dochshpsat  36921  dochkrsat2  36923  lcfl5a  36964  lcfl8a  36970  lclkrlem2a  36974  mapdcnvordN  37125  hdmap14lem4a  37341  hgmapeq0  37374  hdmaplkr  37383  hdmapellkr  37384  extoimad  37650
  Copyright terms: Public domain W3C validator