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

Theorem bitr3d 246
Description: Deduction form of bitr3i 242. (Contributed by NM, 5-Aug-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 192 . 2  |-  ( ph  ->  ( ch  <->  ps )
)
3 bitr3d.2 . 2  |-  ( ph  ->  ( ps  <->  th )
)
42, 3bitrd 244 1  |-  ( ph  ->  ( ch  <->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  3bitrrd  271  3bitr3d  274  3bitr3rd  275  biass  348  sbequ12a  1862  sbco2  2026  sbco3  2028  sbcom  2029  sb9i  2034  sbcom2  2053  sbal1  2065  sbal  2066  csbiebt  3117  copsex2t  4253  copsex2g  4254  ordtri2  4427  onmindif  4482  reusv2lem5  4539  onmindif2  4603  ordunisuc2  4635  dfom2  4658  fnssresb  5356  fcnvres  5418  funimass5  5642  fmptco  5691  cbvfo  5799  isocnv  5827  isoini  5835  isoselem  5838  ovmpt2dxf  5973  caovcanrd  6023  riota2df  6325  ordge1n0  6497  ondif2  6501  oa00  6557  odi  6577  oeoe  6597  eceqoveq  6763  omsucdomOLD  7056  isfinite2  7115  unfilem1  7121  fodomfib  7136  inficl  7178  dffi3  7184  ordiso2  7230  ordtypelem9  7241  cantnfle  7372  cantnf  7395  wemapwe  7400  rankr1a  7508  bnd2  7563  iscard  7608  domtri2  7622  nnsdomel  7623  cardaleph  7716  dfac12lem2  7770  cfss  7891  axcc3  8064  fodomb  8151  iundom2g  8162  inar1  8397  ltpiord  8511  ordpinq  8567  suplem2pr  8677  enreceq  8691  subeq0  9073  negcon1  9099  lesub  9253  ltsub13  9255  subge0  9287  mul0or  9408  div11  9450  divmuleq  9465  ltmuldiv2  9627  lemuldiv2  9636  nn1suc  9767  addltmul  9947  elnnnn0  10007  znn0sub  10065  prime  10092  uzindOLD  10106  zbtwnre  10314  xadddi2  10617  supxrbnd  10647  fz1n  10812  fzrev3  10849  modsubdir  11008  om2uzlt2i  11014  hashf1lem1  11393  cnpart  11725  sqr11  11748  sqrsq2  11754  absdiflt  11801  absdifle  11802  sqreulem  11843  sqreu  11844  eqsqror  11850  clim2  11978  climshft2  12056  isercoll  12141  sumrb  12186  supcvg  12314  sinbnd  12460  cosbnd  12461  sqr2irr  12527  dvdscmulr  12557  dvdsmulcr  12558  oddm1even  12588  bitsmod  12627  bitsinv1lem  12632  isprm3  12767  prmrp  12780  qredeq  12785  crt  12846  pcdvdsb  12921  pceq0  12923  unbenlem  12955  ramcl  13076  pwselbasb  13387  pwsle  13391  imasleval  13443  xpsfrnel2  13467  acsfn  13561  ismon2  13637  isepi2  13644  epii  13646  fthsect  13799  fthmon  13801  isipodrs  14264  ipodrsfi  14266  imasmnd2  14409  gsumval2a  14459  grpid  14517  grplmulf1o  14542  imasgrp2  14610  ghmeqker  14709  ghmf1  14711  gacan  14759  odmulgeq  14870  pgpssslw  14925  efgsfo  15048  efgred  15057  abladdsub4  15115  subgdmdprd  15269  imasrng  15402  lspsnss2  15762  gsumbagdiaglem  16121  znf1o  16505  znfld  16514  znunit  16517  znrrg  16519  iporthcom  16539  ip2eq  16557  obsne0  16625  eltg3  16700  eltop  16712  eltop2  16713  eltop3  16714  lmbrf  16990  cncnpi  17007  dfcon2  17145  1stcfb  17171  elptr  17268  xkoccn  17313  txcn  17320  hausdiag  17339  hmeoimaf1o  17461  isfbas  17524  ufileu  17614  alexsubALTlem4  17744  tsmsf1o  17827  ismet2  17898  imasdsf1olem  17937  imasf1oxmet  17939  imasf1omet  17940  xmseq0  18010  imasf1oxms  18035  nrmmetd  18097  nlmmul0or  18194  xrsxmet  18315  metdseq0  18358  elpi1i  18544  cphsqrcl2  18622  tchcph  18667  lmmbrf  18688  caucfil  18709  lmclim  18728  cmsss  18772  srabn  18777  ovolfioo  18827  ovolficc  18828  elovolmr  18835  ovolctb  18849  ovolicc2lem3  18878  mbfmulc2lem  19002  mbfimaopnlem  19010  itg2mulclem  19101  iblrelem  19145  ellimc2  19227  mdegle0  19463  fta1glem2  19552  dgreq0  19646  plydivlem4  19676  plydivex  19677  fta1  19688  quotcan  19689  logeftb  19937  quad2  20135  cubic2  20144  dquartlem1  20147  atandm4  20175  fsumharmonic  20305  wilthlem1  20306  basellem8  20325  mumullem2  20418  chpchtsum  20458  logfaclbnd  20461  dchrelbas4  20482  lgsne0  20572  lgsqrlem2  20581  lgsdchrval  20586  lgsquadlem1  20593  lgsquadlem2  20594  2sqlem7  20609  dchrisum0lem1  20665  grpoid  20890  grpodiveq  20923  nvsubadd  21213  nvmeq0  21222  nvgt0  21241  imsmetlem  21259  nmlnogt0  21375  ip2eqi  21435  hvaddcan2  21650  hvmulcan2  21652  hvaddsub4  21657  hi2eq  21684  pjhtheu  21973  lnopeqi  22588  riesz1  22645  jpi  22850  chcv2  22936  cvp  22955  atnemeq0  22957  ballotlemfc0  23051  ballotlemfcc  23052  prsspwg  23184  xppreima  23211  fmptcof2  23229  funcnvmptOLD  23234  funcnvmpt  23235  xrge0addgt0  23331  lmlim  23371  eupath2lem3  23903  ghomf1olem  24001  mulcan1g  24084  subeqrev  24092  fz0n  24097  imageval  24469  onsuct0  24880  onint1  24888  areacirclem2  24925  areacirclem3  24926  areacirclem5  24929  areacirc  24931  dffprod  25319  mvecrtol  25473  mvecrtol2  25477  cmp2morp  25958  nn0prpwlem  26238  filnetlem4  26330  isdmn3  26699  rmxycomplete  27002  gicabl  27263  lindfmm  27297  lindsmm  27298  lsslinds  27301  pm14.123b  27626  iotavalb  27630  climreeq  27739  frgra3vlem2  28179  trsbc  28304  bnj1280  29050  lcvp  29230  lcv2  29232  lsatnem0  29235  atnem0  29508  cvlsupr2  29533  cvr2N  29600  athgt  29645  2llnmat  29713  pmap11  29951  pmapeq0  29955  2lnat  29973  paddclN  30031  pmapjat1  30042  ltrn2ateq  30369  dihcnvord  31464  dihcnv11  31465  dih0bN  31471  dih0sb  31475  dihlspsnat  31523  dihatexv2  31529  dihglblem6  31530  dochvalr  31547  dochn0nv  31565  djhcvat42  31605  dochsatshp  31641  dochshpsat  31644  dochkrsat2  31646  lcfl5a  31687  lcfl8a  31693  lclkrlem2a  31697  mapdcnvordN  31848  hdmap14lem4a  32064  hgmapeq0  32097  hdmaplkr  32106  hdmapellkr  32107
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator