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

Theorem bitr3d 247
Description: Deduction form of bitr3i 243. (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 193 . 2  |-  ( ph  ->  ( ch  <->  ps )
)
3 bitr3d.2 . 2  |-  ( ph  ->  ( ps  <->  th )
)
42, 3bitrd 245 1  |-  ( ph  ->  ( ch  <->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  3bitrrd  272  3bitr3d  275  3bitr3rd  276  biass  349  sbequ12a  1946  sbco2  2161  sbco3  2163  sbcom  2164  sb9i  2169  sbcom2  2189  sbal1  2202  sbal  2203  csbiebt  3279  prsspwg  3947  prsspwgOLD  3948  copsex2t  4435  copsex2g  4436  ordtri2  4608  onmindif  4663  reusv2lem5  4720  onmindif2  4784  ordunisuc2  4816  dfom2  4839  fnssresb  5549  fcnvres  5612  funimass5  5839  fmptco  5893  cbvfo  6014  isocnv  6042  isoini  6050  isoselem  6053  ovmpt2dxf  6191  caovcanrd  6242  riota2df  6562  ordge1n0  6734  ondif2  6738  oa00  6794  odi  6814  oeoe  6834  eceqoveq  7001  omsucdomOLD  7294  isfinite2  7357  unfilem1  7363  fodomfib  7378  inficl  7422  dffi3  7428  ordiso2  7476  ordtypelem9  7487  cantnfle  7618  cantnf  7641  wemapwe  7646  rankr1a  7754  bnd2  7809  iscard  7854  domtri2  7868  nnsdomel  7869  cardaleph  7962  dfac12lem2  8016  cfss  8137  axcc3  8310  fodomb  8396  iundom2g  8407  inar1  8642  ltpiord  8756  ordpinq  8812  suplem2pr  8922  enreceq  8936  subeq0  9319  negcon1  9345  lesub  9499  ltsub13  9501  subge0  9533  mul0or  9654  div11  9696  divmuleq  9711  ltmuldiv2  9873  lemuldiv2  9882  nn1suc  10013  addltmul  10195  elnnnn0  10255  znn0sub  10315  prime  10342  uzindOLD  10356  zbtwnre  10564  xadddi2  10868  supxrbnd  10899  fz1n  11065  fzrev3  11103  modsubdir  11277  om2uzlt2i  11283  hashf1lem1  11696  cnpart  12037  sqr11  12060  sqrsq2  12066  absdiflt  12113  absdifle  12114  sqreulem  12155  sqreu  12156  eqsqror  12162  clim2  12290  climshft2  12368  isercoll  12453  sumrb  12499  supcvg  12627  sinbnd  12773  cosbnd  12774  sqr2irr  12840  dvdscmulr  12870  dvdsmulcr  12871  oddm1even  12901  bitsmod  12940  bitsinv1lem  12945  isprm3  13080  prmrp  13093  qredeq  13098  crt  13159  pcdvdsb  13234  pceq0  13236  unbenlem  13268  ramcl  13389  pwselbasb  13702  pwsle  13706  imasleval  13758  xpsfrnel2  13782  acsfn  13876  ismon2  13952  isepi2  13959  epii  13961  fthsect  14114  fthmon  14116  isipodrs  14579  ipodrsfi  14581  imasmnd2  14724  gsumval2a  14774  grpid  14832  grplmulf1o  14857  imasgrp2  14925  ghmeqker  15024  ghmf1  15026  gacan  15074  odmulgeq  15185  pgpssslw  15240  efgsfo  15363  efgred  15372  abladdsub4  15430  subgdmdprd  15584  imasrng  15717  lspsnss2  16073  gsumbagdiaglem  16432  znf1o  16824  znfld  16833  znunit  16836  znrrg  16838  iporthcom  16858  ip2eq  16876  obsne0  16944  eltg3  17019  eltop  17031  eltop2  17032  eltop3  17033  lmbrf  17316  cncnpi  17334  dfcon2  17474  1stcfb  17500  elptr  17597  xkoccn  17643  txcn  17650  hausdiag  17669  hmeoimaf1o  17794  isfbas  17853  ufileu  17943  alexsubALTlem4  18073  tsmsf1o  18166  ismet2  18355  imasdsf1olem  18395  imasf1oxmet  18397  imasf1omet  18398  xmseq0  18486  imasf1oxms  18511  metucnOLD  18610  metucn  18611  nrmmetd  18614  nlmmul0or  18711  xrsxmet  18832  metdseq0  18876  elpi1i  19063  cphsqrcl2  19141  tchcph  19186  lmmbrf  19207  caucfil  19228  lmclim  19247  cmsss  19295  srabn  19306  ovolfioo  19356  ovolficc  19357  elovolmr  19364  ovolctb  19378  ovolicc2lem3  19407  mbfmulc2lem  19531  mbfimaopnlem  19539  itg2mulclem  19630  iblrelem  19674  ellimc2  19756  mdegle0  19992  fta1glem2  20081  dgreq0  20175  plydivlem4  20205  plydivex  20206  fta1  20217  quotcan  20218  logeftb  20470  quad2  20671  cubic2  20680  dquartlem1  20683  atandm4  20711  fsumharmonic  20842  wilthlem1  20843  basellem8  20862  mumullem2  20955  chpchtsum  20995  logfaclbnd  20998  dchrelbas4  21019  lgsne0  21109  lgsqrlem2  21118  lgsdchrval  21123  lgsquadlem1  21130  lgsquadlem2  21131  2sqlem7  21146  dchrisum0lem1  21202  eupath2lem3  21693  grpoid  21803  grpodiveq  21836  nvsubadd  22128  nvmeq0  22137  nvgt0  22156  imsmetlem  22174  nmlnogt0  22290  ip2eqi  22350  hvaddcan2  22565  hvmulcan2  22567  hvaddsub4  22572  hi2eq  22599  pjhtheu  22888  lnopeqi  23503  riesz1  23560  jpi  23765  chcv2  23851  cvp  23870  atnemeq0  23872  fmptcof2  24068  funcnvmptOLD  24074  funcnvmpt  24075  xrge0addgt0  24206  lmlim  24325  ballotlemfc0  24742  ballotlemfcc  24743  ghomf1olem  25097  mulcan1g  25181  subeqrev  25189  fz0n  25194  prodrblem2  25249  imageval  25767  onsuct0  26183  onint1  26191  mblfinlem2  26235  ovoliunnfl  26238  voliunnfl  26240  volsupnfl  26241  mbfresfi  26243  mbfposadd  26244  itg2addnclem  26246  itg2addnclem2  26247  itg2addnc  26249  itg2gt0cn  26250  itgaddnclem2  26254  ftc1anclem5  26274  areacirclem2  26282  areacirclem3  26283  areacirclem5  26286  areacirc  26288  nn0prpwlem  26316  filnetlem4  26401  isdmn3  26675  rmxycomplete  26971  gicabl  27231  lindfmm  27265  lindsmm  27266  lsslinds  27269  pm14.123b  27594  iotavalb  27598  climreeq  27706  frgra3vlem2  28328  trsbc  28562  bnj1280  29326  sbco2wAUX7  29522  sbco3wAUX7  29524  sbcomwAUX7  29525  sbal1NEW7  29552  sbalNEW7  29553  sbcom2NEW7  29581  ax7w6AUX7  29589  ax7w15lemAUX7  29604  sbco2OLD7  29689  sbco3OLD7  29691  sbcomOLD7  29692  sb9iOLD7  29695  lcvp  29775  lcv2  29777  lsatnem0  29780  atnem0  30053  cvlsupr2  30078  cvr2N  30145  athgt  30190  2llnmat  30258  pmap11  30496  pmapeq0  30500  2lnat  30518  paddclN  30576  pmapjat1  30587  ltrn2ateq  30914  dihcnvord  32009  dihcnv11  32010  dih0bN  32016  dih0sb  32020  dihlspsnat  32068  dihatexv2  32074  dihglblem6  32075  dochvalr  32092  dochn0nv  32110  djhcvat42  32150  dochsatshp  32186  dochshpsat  32189  dochkrsat2  32191  lcfl5a  32232  lcfl8a  32238  lclkrlem2a  32242  mapdcnvordN  32393  hdmap14lem4a  32609  hgmapeq0  32642  hdmaplkr  32651  hdmapellkr  32652
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 178
  Copyright terms: Public domain W3C validator