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  1964  sbco2  2134  sbco2OLD  2135  sbco3  2137  sbco3OLD  2138  sb9iOLD  2151  sbcom2  2173  sbcom2OLD  2174  sbal1  2193  sbal1OLD  2194  sbal2  2195  sbal  2196  sbalOLD  2197  csbiebt  3455  prsspwg  4184  reusv2lem5  4652  copsex2t  4734  copsex2g  4735  ordtri2  4913  onmindif  4967  fnssresb  5693  fcnvres  5762  funimass5  5998  fmptco  6054  cbvfo  6180  isocnv  6214  isoini  6222  isoselem  6225  riota2df  6266  ovmpt2dxf  6412  caovcanrd  6462  onmindif2  6631  ordunisuc2  6663  dfom2  6686  ordge1n0  7148  ondif2  7152  oa00  7208  odi  7228  oeoe  7248  eceqoveq  7416  omsucdomOLD  7713  isfinite2  7778  unfilem1  7784  fodomfib  7800  inficl  7885  dffi3  7891  ordiso2  7940  ordtypelem9  7951  cantnfle  8090  cantnf  8112  cantnfleOLD  8120  cantnfOLD  8134  wemapwe  8139  wemapweOLD  8140  rankr1a  8254  bnd2  8311  iscard  8356  domtri2  8370  nnsdomel  8371  cardaleph  8470  dfac12lem2  8524  cfss  8645  axcc3  8818  fodomb  8904  iundom2g  8915  inar1  9153  ltpiord  9265  ordpinq  9321  suplem2pr  9431  enreceq  9443  subeq0  9845  negcon1  9871  subeqrev  9982  lesub  10031  ltsub13  10033  subge0  10065  mul0or  10189  mulcan1g  10202  div11  10233  divmuleq  10249  ltmuldiv2  10416  lemuldiv2  10425  nn1suc  10557  addltmul  10774  elnnnn0  10839  znn0sub  10910  prime  10941  uzindOLD  10955  zbtwnre  11180  xadddi2  11489  supxrbnd  11520  fz1n  11704  fzrev3  11745  fzonlt0  11816  modsubdir  12023  om2uzlt2i  12030  hashf1lem1  12470  cnpart  13036  sqrt11  13059  sqrtsq2  13065  absdiflt  13113  absdifle  13114  sqreulem  13155  sqreu  13156  eqsqrtor  13162  clim2  13290  climshft2  13368  isercoll  13453  sumrb  13498  supcvg  13630  sinbnd  13776  cosbnd  13777  sqrt2irr  13843  dvdscmulr  13873  dvdsmulcr  13874  oddm1even  13906  bitsmod  13945  bitsinv1lem  13950  isprm3  14085  prmrp  14101  qredeq  14106  crt  14167  pcdvdsb  14251  pceq0  14253  unbenlem  14285  ramcl  14406  pwselbasb  14743  pwsle  14747  imasleval  14796  xpsfrnel2  14820  acsfn  14914  ismon2  14990  isepi2  14997  epii  14999  fthsect  15152  fthmon  15154  isipodrs  15648  ipodrsfi  15650  imasmnd2  15776  gsumval2a  15834  grpid  15895  grpidrcan  15913  grpidlcan  15914  grplmulf1o  15922  imasgrp2  15995  ghmeqker  16098  ghmf1  16100  gacan  16148  odmulgeq  16385  pgpssslw  16440  efgsfo  16563  efgred  16572  abladdsub4  16630  subgdmdprd  16883  imasrng  17069  lspsnss2  17451  0rng01eqbi  17720  gsumbagdiaglem  17826  znf1o  18385  znfld  18394  znunit  18397  znrrg  18399  iporthcom  18465  ip2eq  18483  obsne0  18551  lindfmm  18657  lindsmm  18658  lsslinds  18661  eltg3  19258  eltop  19270  eltop2  19271  eltop3  19272  lmbrf  19555  cncnpi  19573  dfcon2  19714  1stcfb  19740  elptr  19837  xkoccn  19883  txcn  19890  hausdiag  19909  hmeoimaf1o  20034  isfbas  20093  ufileu  20183  alexsubALTlem4  20313  tsmsf1o  20410  ismet2  20599  imasdsf1olem  20639  imasf1oxmet  20641  imasf1omet  20642  xmseq0  20730  imasf1oxms  20755  metucnOLD  20854  metucn  20855  nrmmetd  20858  nlmmul0or  20955  xrsxmet  21077  metdseq0  21121  elpi1i  21309  cphsqrtcl2  21396  tchcph  21443  lmmbrf  21464  caucfil  21485  lmclim  21504  cmsss  21552  srabn  21563  ovolfioo  21642  ovolficc  21643  elovolmr  21650  ovolctb  21664  ovolicc2lem3  21693  mbfmulc2lem  21817  mbfimaopnlem  21825  itg2mulclem  21916  iblrelem  21960  ellimc2  22044  mdegle0  22240  fta1glem2  22330  dgreq0  22424  plydivlem4  22454  plydivex  22455  fta1  22466  quotcan  22467  logeftb  22724  quad2  22926  cubic2  22935  dquartlem1  22938  atandm4  22966  fsumharmonic  23097  wilthlem1  23098  basellem8  23117  mumullem2  23210  chpchtsum  23250  logfaclbnd  23253  dchrelbas4  23274  lgsne0  23364  lgsqrlem2  23373  lgsdchrval  23378  lgsquadlem1  23385  lgsquadlem2  23386  2sqlem7  23401  dchrisum0lem1  23457  trgcgrg  23662  tgcolg  23697  lmiinv  23863  eupath2lem3  24683  frgra3vlem2  24705  grpoid  24929  grpodiveq  24962  nvsubadd  25254  nvmeq0  25263  nvgt0  25282  imsmetlem  25300  nmlnogt0  25416  ip2eqi  25476  hvaddcan2  25692  hvmulcan2  25694  hvaddsub4  25699  hi2eq  25726  pjhtheu  26016  lnopeqi  26631  riesz1  26688  jpi  26893  chcv2  26979  cvp  26998  atnemeq0  27000  fmptcof2  27202  funcnvmptOLD  27209  funcnvmpt  27210  nndiffz1  27292  nn0min  27307  xrge0addgt0  27371  lmlim  27593  eulerpartlems  27967  eulerpartlemgh  27985  ballotlemfc0  28099  ballotlemfcc  28100  sgnneg  28147  signsvfpn  28210  signsvfnn  28211  ghomf1olem  28537  fz0n  28613  prodrblem2  28668  imageval  29185  onsuct0  29511  onint1  29519  wl-sbcom2d  29616  wl-sbalnae  29617  wl-ax11-lem8  29637  wl-ax11-lem10  29639  sin2h  29650  tan2h  29652  heicant  29654  mblfinlem3  29658  ovoliunnfl  29661  voliunnfl  29663  volsupnfl  29664  mbfresfi  29666  mbfposadd  29667  dvtanlem  29669  itg2addnclem  29671  itg2addnclem2  29672  itg2addnc  29674  itg2gt0cn  29675  itgaddnclem2  29679  ftc1anclem5  29699  areacirclem1  29712  areacirclem4  29715  areacirc  29717  nn0prpwlem  29745  filnetlem4  29830  isdmn3  30102  rmxycomplete  30485  gicabl  30679  pm14.123b  30939  iotavalb  30943  climreeq  31183  clim2f  31206  ovmpt2rdxf  32024  bnj1280  33173  bj-flbi3  33697  bj-msub  33763  bj-mdiv  33766  lcvp  33855  lcv2  33857  lsatnem0  33860  atnem0  34133  cvlsupr2  34158  cvr2N  34225  athgt  34270  2llnmat  34338  pmap11  34576  pmapeq0  34580  2lnat  34598  paddclN  34656  pmapjat1  34667  ltrn2ateq  34994  dihcnvord  36089  dihcnv11  36090  dih0bN  36096  dih0sb  36100  dihlspsnat  36148  dihatexv2  36154  dihglblem6  36155  dochvalr  36172  dochn0nv  36190  djhcvat42  36230  dochsatshp  36266  dochshpsat  36269  dochkrsat2  36271  lcfl5a  36312  lcfl8a  36318  lclkrlem2a  36322  mapdcnvordN  36473  hdmap14lem4a  36689  hgmapeq0  36722  hdmaplkr  36731  hdmapellkr  36732
  Copyright terms: Public domain W3C validator