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

Theorem bitr3d 263
Description: Deduction form of bitr3i 259. (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 206 . 2  |-  ( ph  ->  ( ch  <->  ps )
)
3 bitr3d.2 . 2  |-  ( ph  ->  ( ps  <->  th )
)
42, 3bitrd 261 1  |-  ( ph  ->  ( ch  <->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189
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 190
This theorem is referenced by:  3bitrrd  288  3bitr3d  291  3bitr3rd  292  biass  366  sbco2  2264  sbco3  2266  sbcom2  2294  sbal1  2309  sbal2  2310  sbal  2311  csbiebt  3369  prsspwg  4121  reusv2lem5  4606  copsex2t  4688  copsex2g  4689  ordtri2  5465  onmindif  5519  fnssresb  5698  fcnvres  5773  foelrni  5927  funimass5  6014  fmptco  6072  cbvfo  6205  isocnv  6239  isoini  6247  isoselem  6250  riota2df  6290  ovmpt2dxf  6441  caovcanrd  6491  onmindif2  6658  ordunisuc2  6690  dfom2  6713  ordge1n0  7218  ondif2  7222  oa00  7278  odi  7298  oeoe  7318  eceqoveq  7486  isfinite2  7847  unfilem1  7853  fodomfib  7869  inficl  7957  dffi3  7963  ordiso2  8048  ordtypelem9  8059  cantnfle  8194  cantnf  8216  wemapwe  8220  rankr1a  8325  bnd2  8382  iscard  8427  domtri2  8441  nnsdomel  8442  cardaleph  8538  dfac12lem2  8592  cfss  8713  axcc3  8886  fodomb  8972  iundom2g  8983  inar1  9218  ltpiord  9330  ordpinq  9386  suplem2pr  9496  enreceq  9508  subeq0  9920  negcon1  9946  subexsub  10059  subeqrev  10063  lesub  10114  ltsub13  10116  subge0  10148  mul0or  10274  mulcan1g  10287  div11  10318  divmuleq  10334  ltmuldiv2  10501  lemuldiv2  10509  nn1suc  10652  addltmul  10871  elnnnn0  10937  znn0sub  11008  prime  11039  zbtwnre  11285  xadddi2  11608  supxrbnd  11639  fz1n  11843  fzrev3  11887  fzo0n  11967  fzonlt0  11968  ico01fl0  12086  modsubdir  12192  om2uzlt2i  12203  hashf1lem1  12659  wrdlenge1n0  12753  cnpart  13380  sqrt11  13403  sqrtsq2  13409  absdiflt  13457  absdifle  13458  sqreulem  13499  sqreu  13500  eqsqrtor  13506  clim2  13645  climshft2  13723  isercoll  13808  sumrb  13856  supcvg  13991  prodrblem2  14062  sinbnd  14311  cosbnd  14312  sqrt2irr  14378  dvdscmulr  14408  dvdsmulcr  14409  oddm1even  14444  bitsmod  14489  bitsinv1lem  14494  isprm3  14712  prmrp  14737  qredeq  14742  crt  14805  pcdvdsb  14897  pceq0  14899  unbenlem  14931  ramcl  15066  pwselbasb  15464  pwsle  15468  imasleval  15525  xpsfrnel2  15549  acsfn  15643  ismon2  15717  isepi2  15724  epii  15726  fthsect  15908  fthmon  15910  isipodrs  16485  ipodrsfi  16487  gsumval2a  16600  imasmnd2  16651  grpid  16779  grpidrcan  16797  grpidlcan  16798  grplmulf1o  16806  imasgrp2  16879  ghmeqker  16987  ghmf1  16989  gacan  17037  odmulgeq  17286  pgpssslw  17344  efgsfo  17467  efgred  17476  abladdsub4  17534  subgdmdprd  17745  imasring  17925  lspsnss2  18306  0ring01eqbi  18574  gsumbagdiaglem  18676  znf1o  19199  znfld  19208  znunit  19211  znrrg  19213  iporthcom  19279  ip2eq  19297  obsne0  19365  lindfmm  19462  lindsmm  19463  lsslinds  19466  eltg3  20054  eltop  20067  eltop2  20068  eltop3  20069  lmbrf  20353  cncnpi  20371  dfcon2  20511  1stcfb  20537  elptr  20665  xkoccn  20711  txcn  20718  hausdiag  20737  hmeoimaf1o  20862  isfbas  20922  ufileu  21012  alexsubALTlem4  21143  tsmsf1o  21237  ismet2  21426  imasdsf1olem  21466  imasf1oxmet  21468  imasf1omet  21469  xmseq0  21557  imasf1oxms  21582  metucn  21664  nrmmetd  21667  nlmmul0or  21764  xrsxmet  21905  metdseq0  21949  metdseq0OLD  21964  elpi1i  22155  cphsqrtcl2  22242  tchcph  22289  lmmbrf  22310  caucfil  22331  lmclim  22350  cmsss  22396  srabn  22405  ovolfioo  22498  ovolficc  22499  elovolmr  22507  ovolctb  22521  ovolicc2lem3  22550  mbfmulc2lem  22682  mbfimaopnlem  22690  itg2mulclem  22783  iblrelem  22827  ellimc2  22911  mdegle0  23105  fta1glem2  23196  dgreq0  23298  plydivlem4  23328  plydivex  23329  fta1  23340  quotcan  23341  logeftb  23612  quad2  23844  cubic2  23853  dquartlem1  23856  atandm4  23884  fsumharmonic  24016  wilthlem1  24072  basellem8  24093  mumullem2  24186  chpchtsum  24226  logfaclbnd  24229  dchrelbas4  24250  lgsne0  24340  lgsqrlem2  24349  lgsdchrval  24354  lgsquadlem1  24361  lgsquadlem2  24362  2sqlem7  24377  dchrisum0lem1  24433  trgcgrg  24639  tgcgr4  24655  tgcolg  24678  lmiinv  24913  iseqlg  24976  eupath2lem3  25786  frgra3vlem2  25808  grpoid  26032  grpodiveq  26065  nvsubadd  26357  nvmeq0  26366  nvgt0  26385  imsmetlem  26403  nmlnogt0  26519  ip2eqi  26579  hvaddcan2  26805  hvmulcan2  26807  hvaddsub4  26812  hi2eq  26839  pjhtheu  27128  lnopeqi  27742  riesz1  27799  jpi  28004  chcv2  28090  cvp  28109  atnemeq0  28111  brabgaf  28292  fmptcof2  28334  funcnvmptOLD  28345  funcnvmpt  28346  nndiffz1  28441  nn0min  28459  xrge0addgt0  28528  smatrcl  28696  lmlim  28827  carsggect  29223  eulerpartlems  29266  eulerpartlemgh  29284  ballotlemfc0  29398  ballotlemfcc  29399  sgnneg  29484  signsvfpn  29546  signsvfnn  29547  bnj1280  29901  elmrsubrn  30230  msubff1  30266  ghomf1olem  30384  fz0n  30436  imageval  30768  nn0prpwlem  31049  filnetlem4  31108  onsuct0  31172  onint1  31180  bj-mdiv  31782  dissneqlem  31812  wl-sbalnae  31962  wl-ax11-lem8  31986  wl-ax11-lem10  31988  sin2h  31999  tan2h  32001  poimirlem18  32022  poimirlem21  32025  poimirlem24  32028  heicant  32039  mblfinlem3  32043  ovoliunnfl  32046  voliunnfl  32048  volsupnfl  32049  mbfresfi  32051  mbfposadd  32052  dvtanlemOLD  32055  itg2addnclem  32057  itg2addnclem2  32058  itg2addnc  32060  itg2gt0cn  32061  itgaddnclem2  32065  ftc1anclem5  32085  areacirclem1  32096  areacirclem4  32099  areacirc  32101  isdmn3  32371  lcvp  32677  lcv2  32679  lsatnem0  32682  atnem0  32955  cvlsupr2  32980  cvr2N  33047  athgt  33092  2llnmat  33160  pmap11  33398  pmapeq0  33402  2lnat  33420  paddclN  33478  pmapjat1  33489  ltrn2ateq  33817  dihcnvord  34913  dihcnv11  34914  dih0bN  34920  dih0sb  34924  dihlspsnat  34972  dihatexv2  34978  dihglblem6  34979  dochvalr  34996  dochn0nv  35014  djhcvat42  35054  dochsatshp  35090  dochshpsat  35093  dochkrsat2  35095  lcfl5a  35136  lcfl8a  35142  lclkrlem2a  35146  mapdcnvordN  35297  hdmap14lem4a  35513  hgmapeq0  35546  hdmaplkr  35555  hdmapellkr  35556  rmxycomplete  35836  gicabl  36028  extoimad  36678  radcnvrat  36733  pm14.123b  36847  iotavalb  36851  climreeq  37790  clim2f  37813  dfodd4  38933  pfxccat3a  39117  ssprss  39148  cusgruvtxb  39654  eupth2lem3lem3  40142  eupth2lem3lem6  40145  nnsgrpnmnd  40326  ovmpt2rdxf  40628
  Copyright terms: Public domain W3C validator