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

Theorem bitr3d 258
Description: Deduction form of bitr3i 254. (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 204 . 2  |-  ( ph  ->  ( ch  <->  ps )
)
3 bitr3d.2 . 2  |-  ( ph  ->  ( ps  <->  th )
)
42, 3bitrd 256 1  |-  ( ph  ->  ( ch  <->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187
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 188
This theorem is referenced by:  3bitrrd  283  3bitr3d  286  3bitr3rd  287  biass  360  sbco2  2213  sbco3  2215  sbcom2  2244  sbal1  2259  sbal2  2260  sbal  2261  csbiebt  3415  prsspwg  4157  reusv2lem5  4629  copsex2t  4707  copsex2g  4708  ordtri2  5477  onmindif  5531  fnssresb  5706  fcnvres  5777  foelrni  5929  funimass5  6014  fmptco  6071  cbvfo  6202  isocnv  6236  isoini  6244  isoselem  6247  riota2df  6287  ovmpt2dxf  6436  caovcanrd  6486  onmindif2  6653  ordunisuc2  6685  dfom2  6708  ordge1n0  7211  ondif2  7215  oa00  7271  odi  7291  oeoe  7311  eceqoveq  7479  isfinite2  7838  unfilem1  7844  fodomfib  7860  inficl  7948  dffi3  7954  ordiso2  8039  ordtypelem9  8050  cantnfle  8184  cantnf  8206  wemapwe  8210  rankr1a  8315  bnd2  8372  iscard  8417  domtri2  8431  nnsdomel  8432  cardaleph  8527  dfac12lem2  8581  cfss  8702  axcc3  8875  fodomb  8961  iundom2g  8972  inar1  9207  ltpiord  9319  ordpinq  9375  suplem2pr  9485  enreceq  9497  subeq0  9907  negcon1  9933  subexsub  10047  subeqrev  10049  lesub  10100  ltsub13  10102  subge0  10134  mul0or  10259  mulcan1g  10272  div11  10303  divmuleq  10319  ltmuldiv2  10486  lemuldiv2  10494  nn1suc  10637  addltmul  10855  elnnnn0  10920  znn0sub  10991  prime  11023  zbtwnre  11269  xadddi2  11590  supxrbnd  11621  fz1n  11824  fzrev3  11868  fzo0n  11947  fzonlt0  11948  ico01fl0  12059  modsubdir  12164  om2uzlt2i  12171  hashf1lem1  12622  wrdlenge1n0  12706  cnpart  13303  sqrt11  13326  sqrtsq2  13332  absdiflt  13380  absdifle  13381  sqreulem  13422  sqreu  13423  eqsqrtor  13429  clim2  13567  climshft2  13645  isercoll  13730  sumrb  13778  supcvg  13913  prodrblem2  13984  sinbnd  14233  cosbnd  14234  sqrt2irr  14300  dvdscmulr  14330  dvdsmulcr  14331  oddm1even  14365  bitsmod  14409  bitsinv1lem  14414  isprm3  14632  prmrp  14657  qredeq  14662  crt  14725  pcdvdsb  14817  pceq0  14819  unbenlem  14851  ramcl  14986  pwselbasb  15385  pwsle  15389  imasleval  15446  xpsfrnel2  15470  acsfn  15564  ismon2  15638  isepi2  15645  epii  15647  fthsect  15829  fthmon  15831  isipodrs  16406  ipodrsfi  16408  gsumval2a  16521  imasmnd2  16572  grpid  16700  grpidrcan  16718  grpidlcan  16719  grplmulf1o  16727  imasgrp2  16800  ghmeqker  16908  ghmf1  16910  gacan  16958  odmulgeq  17207  pgpssslw  17265  efgsfo  17388  efgred  17397  abladdsub4  17455  subgdmdprd  17666  imasring  17846  lspsnss2  18227  0ring01eqbi  18496  gsumbagdiaglem  18598  znf1o  19120  znfld  19129  znunit  19132  znrrg  19134  iporthcom  19200  ip2eq  19218  obsne0  19286  lindfmm  19383  lindsmm  19384  lsslinds  19387  eltg3  19975  eltop  19988  eltop2  19989  eltop3  19990  lmbrf  20274  cncnpi  20292  dfcon2  20432  1stcfb  20458  elptr  20586  xkoccn  20632  txcn  20639  hausdiag  20658  hmeoimaf1o  20783  isfbas  20842  ufileu  20932  alexsubALTlem4  21063  tsmsf1o  21157  ismet2  21346  imasdsf1olem  21386  imasf1oxmet  21388  imasf1omet  21389  xmseq0  21477  imasf1oxms  21502  metucn  21584  nrmmetd  21587  nlmmul0or  21684  xrsxmet  21825  metdseq0  21869  metdseq0OLD  21884  elpi1i  22075  cphsqrtcl2  22162  tchcph  22209  lmmbrf  22230  caucfil  22251  lmclim  22270  cmsss  22316  srabn  22325  ovolfioo  22418  ovolficc  22419  elovolmr  22427  ovolctb  22441  ovolicc2lem3  22470  mbfmulc2lem  22601  mbfimaopnlem  22609  itg2mulclem  22702  iblrelem  22746  ellimc2  22830  mdegle0  23024  fta1glem2  23115  dgreq0  23217  plydivlem4  23247  plydivex  23248  fta1  23259  quotcan  23260  logeftb  23531  quad2  23763  cubic2  23772  dquartlem1  23775  atandm4  23803  fsumharmonic  23935  wilthlem1  23991  basellem8  24012  mumullem2  24105  chpchtsum  24145  logfaclbnd  24148  dchrelbas4  24169  lgsne0  24259  lgsqrlem2  24268  lgsdchrval  24273  lgsquadlem1  24280  lgsquadlem2  24281  2sqlem7  24296  dchrisum0lem1  24352  trgcgrg  24558  tgcgr4  24574  tgcolg  24597  lmiinv  24832  iseqlg  24895  eupath2lem3  25705  frgra3vlem2  25727  grpoid  25949  grpodiveq  25982  nvsubadd  26274  nvmeq0  26283  nvgt0  26302  imsmetlem  26320  nmlnogt0  26436  ip2eqi  26496  hvaddcan2  26722  hvmulcan2  26724  hvaddsub4  26729  hi2eq  26756  pjhtheu  27045  lnopeqi  27659  riesz1  27716  jpi  27921  chcv2  28007  cvp  28026  atnemeq0  28028  brabgaf  28218  fmptcof2  28261  funcnvmptOLD  28272  funcnvmpt  28273  nndiffz1  28372  nn0min  28391  xrge0addgt0  28461  smatrcl  28630  lmlim  28761  carsggect  29158  eulerpartlems  29201  eulerpartlemgh  29219  ballotlemfc0  29333  ballotlemfcc  29334  sgnneg  29419  signsvfpn  29482  signsvfnn  29483  bnj1280  29837  elmrsubrn  30166  msubff1  30202  ghomf1olem  30320  fz0n  30371  imageval  30702  nn0prpwlem  30983  filnetlem4  31042  onsuct0  31106  onint1  31114  bj-mdiv  31676  dissneqlem  31706  wl-sbalnae  31856  wl-ax11-lem8  31886  wl-ax11-lem10  31888  sin2h  31899  tan2h  31901  poimirlem18  31922  poimirlem21  31925  poimirlem24  31928  heicant  31939  mblfinlem3  31943  ovoliunnfl  31946  voliunnfl  31948  volsupnfl  31949  mbfresfi  31951  mbfposadd  31952  dvtanlemOLD  31955  itg2addnclem  31957  itg2addnclem2  31958  itg2addnc  31960  itg2gt0cn  31961  itgaddnclem2  31965  ftc1anclem5  31985  areacirclem1  31996  areacirclem4  31999  areacirc  32001  isdmn3  32271  lcvp  32575  lcv2  32577  lsatnem0  32580  atnem0  32853  cvlsupr2  32878  cvr2N  32945  athgt  32990  2llnmat  33058  pmap11  33296  pmapeq0  33300  2lnat  33318  paddclN  33376  pmapjat1  33387  ltrn2ateq  33715  dihcnvord  34811  dihcnv11  34812  dih0bN  34818  dih0sb  34822  dihlspsnat  34870  dihatexv2  34876  dihglblem6  34877  dochvalr  34894  dochn0nv  34912  djhcvat42  34952  dochsatshp  34988  dochshpsat  34991  dochkrsat2  34993  lcfl5a  35034  lcfl8a  35040  lclkrlem2a  35044  mapdcnvordN  35195  hdmap14lem4a  35411  hgmapeq0  35444  hdmaplkr  35453  hdmapellkr  35454  rmxycomplete  35735  gicabl  35927  extoimad  36577  radcnvrat  36633  pm14.123b  36747  iotavalb  36751  climreeq  37633  clim2f  37656  dfodd4  38658  pfxccat3a  38840  ssprss  38867  cusgruvtxb  39246  nnsgrpnmnd  39437  ovmpt2rdxf  39741
  Copyright terms: Public domain W3C validator