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  1951  sbco2  2121  sbco2OLD  2122  sbco3  2124  sbco3OLD  2125  sb9iOLD  2138  sbcom2  2160  sbcom2OLD  2161  sbal1  2180  sbal1OLD  2181  sbal2  2182  sbal  2183  sbalOLD  2184  csbiebt  3414  prsspwg  4137  reusv2lem5  4604  copsex2t  4685  copsex2g  4686  ordtri2  4861  onmindif  4915  fnssresb  5630  fcnvres  5695  funimass5  5928  fmptco  5984  cbvfo  6101  isocnv  6129  isoini  6137  isoselem  6140  riota2df  6181  ovmpt2dxf  6325  caovcanrd  6375  onmindif2  6532  ordunisuc2  6564  dfom2  6587  ordge1n0  7047  ondif2  7051  oa00  7107  odi  7127  oeoe  7147  eceqoveq  7314  omsucdomOLD  7616  isfinite2  7680  unfilem1  7686  fodomfib  7701  inficl  7785  dffi3  7791  ordiso2  7839  ordtypelem9  7850  cantnfle  7989  cantnf  8011  cantnfleOLD  8019  cantnfOLD  8033  wemapwe  8038  wemapweOLD  8039  rankr1a  8153  bnd2  8210  iscard  8255  domtri2  8269  nnsdomel  8270  cardaleph  8369  dfac12lem2  8423  cfss  8544  axcc3  8717  fodomb  8803  iundom2g  8814  inar1  9052  ltpiord  9166  ordpinq  9222  suplem2pr  9332  enreceq  9346  subeq0  9745  negcon1  9771  subeqrev  9881  lesub  9928  ltsub13  9930  subge0  9962  mul0or  10086  mulcan1g  10099  div11  10130  divmuleq  10146  ltmuldiv2  10313  lemuldiv2  10322  nn1suc  10453  addltmul  10670  elnnnn0  10733  znn0sub  10802  prime  10832  uzindOLD  10846  zbtwnre  11061  xadddi2  11370  supxrbnd  11401  fz1n  11584  fzrev3  11638  fzonlt0  11688  modsubdir  11883  om2uzlt2i  11890  hashf1lem1  12325  cnpart  12846  sqr11  12869  sqrsq2  12875  absdiflt  12922  absdifle  12923  sqreulem  12964  sqreu  12965  eqsqror  12971  clim2  13099  climshft2  13177  isercoll  13262  sumrb  13307  supcvg  13435  sinbnd  13581  cosbnd  13582  sqr2irr  13648  dvdscmulr  13678  dvdsmulcr  13679  oddm1even  13710  bitsmod  13749  bitsinv1lem  13754  isprm3  13889  prmrp  13904  qredeq  13909  crt  13970  pcdvdsb  14052  pceq0  14054  unbenlem  14086  ramcl  14207  pwselbasb  14544  pwsle  14548  imasleval  14597  xpsfrnel2  14621  acsfn  14715  ismon2  14791  isepi2  14798  epii  14800  fthsect  14953  fthmon  14955  isipodrs  15449  ipodrsfi  15451  imasmnd2  15576  gsumval2a  15630  grpid  15691  grpidrcan  15709  grpidlcan  15710  grplmulf1o  15718  imasgrp2  15788  ghmeqker  15891  ghmf1  15893  gacan  15941  odmulgeq  16178  pgpssslw  16233  efgsfo  16356  efgred  16365  abladdsub4  16423  subgdmdprd  16652  imasrng  16833  lspsnss2  17208  gsumbagdiaglem  17567  znf1o  18108  znfld  18117  znunit  18120  znrrg  18122  iporthcom  18188  ip2eq  18206  obsne0  18274  lindfmm  18380  lindsmm  18381  lsslinds  18384  eltg3  18698  eltop  18710  eltop2  18711  eltop3  18712  lmbrf  18995  cncnpi  19013  dfcon2  19154  1stcfb  19180  elptr  19277  xkoccn  19323  txcn  19330  hausdiag  19349  hmeoimaf1o  19474  isfbas  19533  ufileu  19623  alexsubALTlem4  19753  tsmsf1o  19850  ismet2  20039  imasdsf1olem  20079  imasf1oxmet  20081  imasf1omet  20082  xmseq0  20170  imasf1oxms  20195  metucnOLD  20294  metucn  20295  nrmmetd  20298  nlmmul0or  20395  xrsxmet  20517  metdseq0  20561  elpi1i  20749  cphsqrcl2  20836  tchcph  20883  lmmbrf  20904  caucfil  20925  lmclim  20944  cmsss  20992  srabn  21003  ovolfioo  21082  ovolficc  21083  elovolmr  21090  ovolctb  21104  ovolicc2lem3  21133  mbfmulc2lem  21257  mbfimaopnlem  21265  itg2mulclem  21356  iblrelem  21400  ellimc2  21484  mdegle0  21680  fta1glem2  21770  dgreq0  21864  plydivlem4  21894  plydivex  21895  fta1  21906  quotcan  21907  logeftb  22164  quad2  22366  cubic2  22375  dquartlem1  22378  atandm4  22406  fsumharmonic  22537  wilthlem1  22538  basellem8  22557  mumullem2  22650  chpchtsum  22690  logfaclbnd  22693  dchrelbas4  22714  lgsne0  22804  lgsqrlem2  22813  lgsdchrval  22818  lgsquadlem1  22825  lgsquadlem2  22826  2sqlem7  22841  dchrisum0lem1  22897  trgcgrg  23102  tgcolg  23123  eupath2lem3  23751  grpoid  23861  grpodiveq  23894  nvsubadd  24186  nvmeq0  24195  nvgt0  24214  imsmetlem  24232  nmlnogt0  24348  ip2eqi  24408  hvaddcan2  24624  hvmulcan2  24626  hvaddsub4  24631  hi2eq  24658  pjhtheu  24948  lnopeqi  25563  riesz1  25620  jpi  25825  chcv2  25911  cvp  25930  atnemeq0  25932  fmptcof2  26129  funcnvmptOLD  26136  funcnvmpt  26137  nndiffz1  26219  nn0min  26234  xrge0addgt0  26298  lmlim  26521  eulerpartlems  26886  eulerpartlemgh  26904  ballotlemfc0  27018  ballotlemfcc  27019  sgnneg  27066  signsvfpn  27129  signsvfnn  27130  ghomf1olem  27456  fz0n  27532  prodrblem2  27587  imageval  28104  onsuct0  28430  onint1  28438  wl-sbcom2d  28534  wl-sbalnae  28535  wl-ax11-lem8  28555  wl-ax11-lem10  28557  sin2h  28569  tan2h  28571  heicant  28573  mblfinlem3  28577  ovoliunnfl  28580  voliunnfl  28582  volsupnfl  28583  mbfresfi  28585  mbfposadd  28586  dvtanlem  28588  itg2addnclem  28590  itg2addnclem2  28591  itg2addnc  28593  itg2gt0cn  28594  itgaddnclem2  28598  ftc1anclem5  28618  areacirclem1  28631  areacirclem4  28634  areacirc  28636  nn0prpwlem  28664  filnetlem4  28749  isdmn3  29021  rmxycomplete  29405  gicabl  29601  pm14.123b  29827  iotavalb  29831  climreeq  29933  frgra3vlem2  30740  ovmpt2rdxf  30876  bnj1280  32328  bj-flbi3  32850  bj-msub  32916  bj-mdiv  32919  lcvp  33008  lcv2  33010  lsatnem0  33013  atnem0  33286  cvlsupr2  33311  cvr2N  33378  athgt  33423  2llnmat  33491  pmap11  33729  pmapeq0  33733  2lnat  33751  paddclN  33809  pmapjat1  33820  ltrn2ateq  34147  dihcnvord  35242  dihcnv11  35243  dih0bN  35249  dih0sb  35253  dihlspsnat  35301  dihatexv2  35307  dihglblem6  35308  dochvalr  35325  dochn0nv  35343  djhcvat42  35383  dochsatshp  35419  dochshpsat  35422  dochkrsat2  35424  lcfl5a  35465  lcfl8a  35471  lclkrlem2a  35475  mapdcnvordN  35626  hdmap14lem4a  35842  hgmapeq0  35875  hdmaplkr  35884  hdmapellkr  35885
  Copyright terms: Public domain W3C validator