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  2210  sbco3  2212  sbcom2  2241  sbal1  2256  sbal2  2257  sbal  2258  csbiebt  3421  prsspwg  4160  reusv2lem5  4630  copsex2t  4708  copsex2g  4709  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  7208  ondif2  7212  oa00  7268  odi  7288  oeoe  7308  eceqoveq  7476  isfinite2  7835  unfilem1  7841  fodomfib  7857  inficl  7945  dffi3  7951  ordiso2  8030  ordtypelem9  8041  cantnfle  8175  cantnf  8197  wemapwe  8201  rankr1a  8306  bnd2  8363  iscard  8408  domtri2  8422  nnsdomel  8423  cardaleph  8518  dfac12lem2  8572  cfss  8693  axcc3  8866  fodomb  8952  iundom2g  8963  inar1  9199  ltpiord  9311  ordpinq  9367  suplem2pr  9477  enreceq  9489  subeq0  9899  negcon1  9925  subexsub  10039  subeqrev  10041  lesub  10092  ltsub13  10094  subge0  10126  mul0or  10251  mulcan1g  10264  div11  10295  divmuleq  10311  ltmuldiv2  10478  lemuldiv2  10486  nn1suc  10630  addltmul  10848  elnnnn0  10913  znn0sub  10984  prime  11016  zbtwnre  11262  xadddi2  11583  supxrbnd  11614  fz1n  11815  fzrev3  11859  fzo0n  11938  fzonlt0  11939  ico01fl0  12050  modsubdir  12155  om2uzlt2i  12162  hashf1lem1  12613  wrdlenge1n0  12689  cnpart  13282  sqrt11  13305  sqrtsq2  13311  absdiflt  13359  absdifle  13360  sqreulem  13401  sqreu  13402  eqsqrtor  13408  clim2  13546  climshft2  13624  isercoll  13709  sumrb  13757  supcvg  13892  prodrblem2  13963  sinbnd  14212  cosbnd  14213  sqrt2irr  14279  dvdscmulr  14309  dvdsmulcr  14310  oddm1even  14344  bitsmod  14384  bitsinv1lem  14389  isprm3  14595  prmrp  14620  qredeq  14625  crt  14686  pcdvdsb  14772  pceq0  14774  unbenlem  14806  ramcl  14941  pwselbasb  15336  pwsle  15340  imasleval  15389  xpsfrnel2  15413  acsfn  15507  ismon2  15581  isepi2  15588  epii  15590  fthsect  15772  fthmon  15774  isipodrs  16349  ipodrsfi  16351  gsumval2a  16464  imasmnd2  16515  grpid  16643  grpidrcan  16661  grpidlcan  16662  grplmulf1o  16670  imasgrp2  16743  ghmeqker  16851  ghmf1  16853  gacan  16901  odmulgeq  17137  pgpssslw  17192  efgsfo  17315  efgred  17324  abladdsub4  17382  subgdmdprd  17593  imasring  17773  lspsnss2  18154  0ring01eqbi  18423  gsumbagdiaglem  18525  znf1o  19044  znfld  19053  znunit  19056  znrrg  19058  iporthcom  19124  ip2eq  19142  obsne0  19210  lindfmm  19307  lindsmm  19308  lsslinds  19311  eltg3  19899  eltop  19912  eltop2  19913  eltop3  19914  lmbrf  20198  cncnpi  20216  dfcon2  20356  1stcfb  20382  elptr  20510  xkoccn  20556  txcn  20563  hausdiag  20582  hmeoimaf1o  20707  isfbas  20766  ufileu  20856  alexsubALTlem4  20987  tsmsf1o  21081  ismet2  21270  imasdsf1olem  21310  imasf1oxmet  21312  imasf1omet  21313  xmseq0  21401  imasf1oxms  21426  metucn  21508  nrmmetd  21511  nlmmul0or  21608  xrsxmet  21729  metdseq0  21773  elpi1i  21961  cphsqrtcl2  22048  tchcph  22095  lmmbrf  22116  caucfil  22137  lmclim  22156  cmsss  22202  srabn  22211  ovolfioo  22290  ovolficc  22291  elovolmr  22298  ovolctb  22312  ovolicc2lem3  22341  mbfmulc2lem  22471  mbfimaopnlem  22479  itg2mulclem  22572  iblrelem  22616  ellimc2  22700  mdegle0  22894  fta1glem2  22983  dgreq0  23078  plydivlem4  23108  plydivex  23109  fta1  23120  quotcan  23121  logeftb  23389  quad2  23621  cubic2  23630  dquartlem1  23633  atandm4  23661  fsumharmonic  23793  wilthlem1  23849  basellem8  23868  mumullem2  23961  chpchtsum  24001  logfaclbnd  24004  dchrelbas4  24025  lgsne0  24115  lgsqrlem2  24124  lgsdchrval  24129  lgsquadlem1  24136  lgsquadlem2  24137  2sqlem7  24152  dchrisum0lem1  24208  trgcgrg  24413  tgcolg  24450  lmiinv  24681  eupath2lem3  25543  frgra3vlem2  25565  grpoid  25787  grpodiveq  25820  nvsubadd  26112  nvmeq0  26121  nvgt0  26140  imsmetlem  26158  nmlnogt0  26274  ip2eqi  26334  hvaddcan2  26550  hvmulcan2  26552  hvaddsub4  26557  hi2eq  26584  pjhtheu  26873  lnopeqi  27487  riesz1  27544  jpi  27749  chcv2  27835  cvp  27854  atnemeq0  27856  brabgaf  28046  fmptcof2  28090  funcnvmptOLD  28101  funcnvmpt  28102  nndiffz1  28193  nn0min  28213  xrge0addgt0  28283  smatrcl  28452  lmlim  28583  carsggect  28970  eulerpartlems  29010  eulerpartlemgh  29028  ballotlemfc0  29142  ballotlemfcc  29143  sgnneg  29190  signsvfpn  29253  signsvfnn  29254  bnj1280  29608  elmrsubrn  29937  msubff1  29973  ghomf1olem  30091  fz0n  30142  imageval  30473  nn0prpwlem  30754  filnetlem4  30813  onsuct0  30877  onint1  30885  bj-mdiv  31448  dissneqlem  31467  wl-sbalnae  31590  wl-ax11-lem8  31616  wl-ax11-lem10  31618  sin2h  31629  tan2h  31631  poimirlem18  31652  poimirlem21  31655  poimirlem24  31658  heicant  31669  mblfinlem3  31673  ovoliunnfl  31676  voliunnfl  31678  volsupnfl  31679  mbfresfi  31681  mbfposadd  31682  dvtanlemOLD  31685  itg2addnclem  31687  itg2addnclem2  31688  itg2addnc  31690  itg2gt0cn  31691  itgaddnclem2  31695  ftc1anclem5  31715  areacirclem1  31726  areacirclem4  31729  areacirc  31731  isdmn3  32001  lcvp  32305  lcv2  32307  lsatnem0  32310  atnem0  32583  cvlsupr2  32608  cvr2N  32675  athgt  32720  2llnmat  32788  pmap11  33026  pmapeq0  33030  2lnat  33048  paddclN  33106  pmapjat1  33117  ltrn2ateq  33445  dihcnvord  34541  dihcnv11  34542  dih0bN  34548  dih0sb  34552  dihlspsnat  34600  dihatexv2  34606  dihglblem6  34607  dochvalr  34624  dochn0nv  34642  djhcvat42  34682  dochsatshp  34718  dochshpsat  34721  dochkrsat2  34723  lcfl5a  34764  lcfl8a  34770  lclkrlem2a  34774  mapdcnvordN  34925  hdmap14lem4a  35141  hgmapeq0  35174  hdmaplkr  35183  hdmapellkr  35184  rmxycomplete  35461  gicabl  35653  extoimad  36234  radcnvrat  36290  pm14.123b  36404  iotavalb  36408  climreeq  37255  clim2f  37278  dfodd4  38168  pfxccat3a  38350  nnsgrpnmnd  38566  ovmpt2rdxf  38870
  Copyright terms: Public domain W3C validator