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  357  sbco2  2162  sbco3  2164  sbcom2  2193  sbal1  2208  sbal2  2209  sbal  2210  csbiebt  3368  prsspwg  4101  reusv2lem5  4570  copsex2t  4648  copsex2g  4649  ordtri2  4827  onmindif  4881  fnssresb  5601  fcnvres  5670  foelrni  5822  funimass5  5906  fmptco  5966  cbvfo  6093  isocnv  6127  isoini  6135  isoselem  6138  riota2df  6178  ovmpt2dxf  6327  caovcanrd  6377  onmindif2  6546  ordunisuc2  6578  dfom2  6601  ordge1n0  7066  ondif2  7070  oa00  7126  odi  7146  oeoe  7166  eceqoveq  7334  isfinite2  7693  unfilem1  7699  fodomfib  7715  inficl  7800  dffi3  7806  ordiso2  7855  ordtypelem9  7866  cantnfle  8003  cantnf  8025  cantnfleOLD  8033  cantnfOLD  8047  wemapwe  8052  wemapweOLD  8053  rankr1a  8167  bnd2  8224  iscard  8269  domtri2  8283  nnsdomel  8284  cardaleph  8383  dfac12lem2  8437  cfss  8558  axcc3  8731  fodomb  8817  iundom2g  8828  inar1  9064  ltpiord  9176  ordpinq  9232  suplem2pr  9342  enreceq  9354  subeq0  9758  negcon1  9784  subexsub  9898  subeqrev  9900  lesub  9949  ltsub13  9951  subge0  9983  mul0or  10106  mulcan1g  10119  div11  10150  divmuleq  10166  ltmuldiv2  10333  lemuldiv2  10341  nn1suc  10473  addltmul  10691  elnnnn0  10756  znn0sub  10828  prime  10860  zbtwnre  11099  xadddi2  11410  supxrbnd  11441  fz1n  11625  fzrev3  11667  fzo0n  11742  fzonlt0  11743  ico01fl0  11853  modsubdir  11958  om2uzlt2i  11965  hashf1lem1  12408  wrdlenge1n0  12484  cnpart  13075  sqrt11  13098  sqrtsq2  13104  absdiflt  13152  absdifle  13153  sqreulem  13194  sqreu  13195  eqsqrtor  13201  clim2  13329  climshft2  13407  isercoll  13492  sumrb  13537  supcvg  13669  prodrblem2  13740  sinbnd  13917  cosbnd  13918  sqrt2irr  13984  dvdscmulr  14014  dvdsmulcr  14015  oddm1even  14049  bitsmod  14088  bitsinv1lem  14093  isprm3  14228  prmrp  14244  qredeq  14249  crt  14310  pcdvdsb  14394  pceq0  14396  unbenlem  14428  ramcl  14549  pwselbasb  14895  pwsle  14899  imasleval  14948  xpsfrnel2  14972  acsfn  15066  ismon2  15140  isepi2  15147  epii  15149  fthsect  15331  fthmon  15333  isipodrs  15908  ipodrsfi  15910  gsumval2a  16023  imasmnd2  16074  grpid  16202  grpidrcan  16220  grpidlcan  16221  grplmulf1o  16229  imasgrp2  16302  ghmeqker  16410  ghmf1  16412  gacan  16460  odmulgeq  16696  pgpssslw  16751  efgsfo  16874  efgred  16883  abladdsub4  16941  subgdmdprd  17194  imasring  17381  lspsnss2  17764  0ring01eqbi  18034  gsumbagdiaglem  18140  znf1o  18681  znfld  18690  znunit  18693  znrrg  18695  iporthcom  18761  ip2eq  18779  obsne0  18847  lindfmm  18947  lindsmm  18948  lsslinds  18951  eltg3  19548  eltop  19561  eltop2  19562  eltop3  19563  lmbrf  19847  cncnpi  19865  dfcon2  20005  1stcfb  20031  elptr  20159  xkoccn  20205  txcn  20212  hausdiag  20231  hmeoimaf1o  20356  isfbas  20415  ufileu  20505  alexsubALTlem4  20635  tsmsf1o  20732  ismet2  20921  imasdsf1olem  20961  imasf1oxmet  20963  imasf1omet  20964  xmseq0  21052  imasf1oxms  21077  metucnOLD  21176  metucn  21177  nrmmetd  21180  nlmmul0or  21277  xrsxmet  21399  metdseq0  21443  elpi1i  21631  cphsqrtcl2  21718  tchcph  21765  lmmbrf  21786  caucfil  21807  lmclim  21826  cmsss  21874  srabn  21885  ovolfioo  21964  ovolficc  21965  elovolmr  21972  ovolctb  21986  ovolicc2lem3  22015  mbfmulc2lem  22139  mbfimaopnlem  22147  itg2mulclem  22238  iblrelem  22282  ellimc2  22366  mdegle0  22562  fta1glem2  22652  dgreq0  22747  plydivlem4  22777  plydivex  22778  fta1  22789  quotcan  22790  logeftb  23056  quad2  23286  cubic2  23295  dquartlem1  23298  atandm4  23326  fsumharmonic  23458  wilthlem1  23459  basellem8  23478  mumullem2  23571  chpchtsum  23611  logfaclbnd  23614  dchrelbas4  23635  lgsne0  23725  lgsqrlem2  23734  lgsdchrval  23739  lgsquadlem1  23746  lgsquadlem2  23747  2sqlem7  23762  dchrisum0lem1  23818  trgcgrg  24026  tgcolg  24061  lmiinv  24278  eupath2lem3  25100  frgra3vlem2  25122  grpoid  25342  grpodiveq  25375  nvsubadd  25667  nvmeq0  25676  nvgt0  25695  imsmetlem  25713  nmlnogt0  25829  ip2eqi  25889  hvaddcan2  26105  hvmulcan2  26107  hvaddsub4  26112  hi2eq  26139  pjhtheu  26429  lnopeqi  27043  riesz1  27100  jpi  27305  chcv2  27391  cvp  27410  atnemeq0  27412  brabgaf  27595  fmptcof2  27643  funcnvmptOLD  27655  funcnvmpt  27656  nndiffz1  27749  nn0min  27764  xrge0addgt0  27834  lmlim  28083  carsggect  28445  eulerpartlems  28482  eulerpartlemgh  28500  ballotlemfc0  28614  ballotlemfcc  28615  sgnneg  28662  signsvfpn  28725  signsvfnn  28726  elmrsubrn  29069  msubff1  29105  ghomf1olem  29223  fz0n  29276  imageval  29733  onsuct0  30059  onint1  30067  wl-sbalnae  30177  wl-ax11-lem8  30197  wl-ax11-lem10  30199  sin2h  30210  tan2h  30212  heicant  30214  mblfinlem3  30218  ovoliunnfl  30221  voliunnfl  30223  volsupnfl  30224  mbfresfi  30226  mbfposadd  30227  dvtanlemOLD  30230  itg2addnclem  30232  itg2addnclem2  30233  itg2addnc  30235  itg2gt0cn  30236  itgaddnclem2  30240  ftc1anclem5  30260  areacirclem1  30273  areacirclem4  30276  areacirc  30278  nn0prpwlem  30306  filnetlem4  30365  isdmn3  30637  rmxycomplete  31018  gicabl  31215  radcnvrat  31363  pm14.123b  31501  iotavalb  31505  climreeq  31785  clim2f  31808  dfodd4  32501  pfxccat3a  32604  nnsgrpnmnd  32824  ovmpt2rdxf  33128  bnj1280  34423  bj-mdiv  35020  lcvp  35178  lcv2  35180  lsatnem0  35183  atnem0  35456  cvlsupr2  35481  cvr2N  35548  athgt  35593  2llnmat  35661  pmap11  35899  pmapeq0  35903  2lnat  35921  paddclN  35979  pmapjat1  35990  ltrn2ateq  36318  dihcnvord  37414  dihcnv11  37415  dih0bN  37421  dih0sb  37425  dihlspsnat  37473  dihatexv2  37479  dihglblem6  37480  dochvalr  37497  dochn0nv  37515  djhcvat42  37555  dochsatshp  37591  dochshpsat  37594  dochkrsat2  37596  lcfl5a  37637  lcfl8a  37643  lclkrlem2a  37647  mapdcnvordN  37798  hdmap14lem4a  38014  hgmapeq0  38047  hdmaplkr  38056  hdmapellkr  38057  extoimad  38510
  Copyright terms: Public domain W3C validator