MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bitr3d 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  1935  sbco2  2120  sbco3  2122  sbcom  2123  sb9i  2128  sbcom2  2148  sbal1  2161  sbal  2162  csbiebt  3231  prsspwg  3899  prsspwgOLD  3900  copsex2t  4385  copsex2g  4386  ordtri2  4558  onmindif  4612  reusv2lem5  4669  onmindif2  4733  ordunisuc2  4765  dfom2  4788  fnssresb  5498  fcnvres  5561  funimass5  5787  fmptco  5841  cbvfo  5962  isocnv  5990  isoini  5998  isoselem  6001  ovmpt2dxf  6139  caovcanrd  6190  riota2df  6507  ordge1n0  6679  ondif2  6683  oa00  6739  odi  6759  oeoe  6779  eceqoveq  6946  omsucdomOLD  7239  isfinite2  7302  unfilem1  7308  fodomfib  7323  inficl  7366  dffi3  7372  ordiso2  7418  ordtypelem9  7429  cantnfle  7560  cantnf  7583  wemapwe  7588  rankr1a  7696  bnd2  7751  iscard  7796  domtri2  7810  nnsdomel  7811  cardaleph  7904  dfac12lem2  7958  cfss  8079  axcc3  8252  fodomb  8338  iundom2g  8349  inar1  8584  ltpiord  8698  ordpinq  8754  suplem2pr  8864  enreceq  8878  subeq0  9260  negcon1  9286  lesub  9440  ltsub13  9442  subge0  9474  mul0or  9595  div11  9637  divmuleq  9652  ltmuldiv2  9814  lemuldiv2  9823  nn1suc  9954  addltmul  10136  elnnnn0  10196  znn0sub  10256  prime  10283  uzindOLD  10297  zbtwnre  10505  xadddi2  10809  supxrbnd  10840  fz1n  11006  fzrev3  11043  modsubdir  11213  om2uzlt2i  11219  hashf1lem1  11632  cnpart  11973  sqr11  11996  sqrsq2  12002  absdiflt  12049  absdifle  12050  sqreulem  12091  sqreu  12092  eqsqror  12098  clim2  12226  climshft2  12304  isercoll  12389  sumrb  12435  supcvg  12563  sinbnd  12709  cosbnd  12710  sqr2irr  12776  dvdscmulr  12806  dvdsmulcr  12807  oddm1even  12837  bitsmod  12876  bitsinv1lem  12881  isprm3  13016  prmrp  13029  qredeq  13034  crt  13095  pcdvdsb  13170  pceq0  13172  unbenlem  13204  ramcl  13325  pwselbasb  13638  pwsle  13642  imasleval  13694  xpsfrnel2  13718  acsfn  13812  ismon2  13888  isepi2  13895  epii  13897  fthsect  14050  fthmon  14052  isipodrs  14515  ipodrsfi  14517  imasmnd2  14660  gsumval2a  14710  grpid  14768  grplmulf1o  14793  imasgrp2  14861  ghmeqker  14960  ghmf1  14962  gacan  15010  odmulgeq  15121  pgpssslw  15176  efgsfo  15299  efgred  15308  abladdsub4  15366  subgdmdprd  15520  imasrng  15653  lspsnss2  16009  gsumbagdiaglem  16368  znf1o  16756  znfld  16765  znunit  16768  znrrg  16770  iporthcom  16790  ip2eq  16808  obsne0  16876  eltg3  16951  eltop  16963  eltop2  16964  eltop3  16965  lmbrf  17247  cncnpi  17265  dfcon2  17404  1stcfb  17430  elptr  17527  xkoccn  17573  txcn  17580  hausdiag  17599  hmeoimaf1o  17724  isfbas  17783  ufileu  17873  alexsubALTlem4  18003  tsmsf1o  18096  ismet2  18273  imasdsf1olem  18312  imasf1oxmet  18314  imasf1omet  18315  xmseq0  18385  imasf1oxms  18410  metucn  18491  nrmmetd  18494  nlmmul0or  18591  xrsxmet  18712  metdseq0  18756  elpi1i  18943  cphsqrcl2  19021  tchcph  19066  lmmbrf  19087  caucfil  19108  lmclim  19127  cmsss  19173  srabn  19182  ovolfioo  19232  ovolficc  19233  elovolmr  19240  ovolctb  19254  ovolicc2lem3  19283  mbfmulc2lem  19407  mbfimaopnlem  19415  itg2mulclem  19506  iblrelem  19550  ellimc2  19632  mdegle0  19868  fta1glem2  19957  dgreq0  20051  plydivlem4  20081  plydivex  20082  fta1  20093  quotcan  20094  logeftb  20346  quad2  20547  cubic2  20556  dquartlem1  20559  atandm4  20587  fsumharmonic  20718  wilthlem1  20719  basellem8  20738  mumullem2  20831  chpchtsum  20871  logfaclbnd  20874  dchrelbas4  20895  lgsne0  20985  lgsqrlem2  20994  lgsdchrval  20999  lgsquadlem1  21006  lgsquadlem2  21007  2sqlem7  21022  dchrisum0lem1  21078  eupath2lem3  21550  grpoid  21660  grpodiveq  21693  nvsubadd  21985  nvmeq0  21994  nvgt0  22013  imsmetlem  22031  nmlnogt0  22147  ip2eqi  22207  hvaddcan2  22422  hvmulcan2  22424  hvaddsub4  22429  hi2eq  22456  pjhtheu  22745  lnopeqi  23360  riesz1  23417  jpi  23622  chcv2  23708  cvp  23727  atnemeq0  23729  fmptcof2  23919  funcnvmptOLD  23924  funcnvmpt  23925  xrge0addgt0  24044  lmlim  24138  ballotlemfc0  24530  ballotlemfcc  24531  ghomf1olem  24885  mulcan1g  24969  subeqrev  24977  fz0n  24982  prodrblem2  25037  imageval  25494  onsuct0  25906  onint1  25914  ovoliunnfl  25954  voliunnfl  25956  volsupnfl  25957  itg2addnclem  25958  itg2addnclem2  25959  itg2addnc  25960  itg2gt0cn  25961  itgaddnclem2  25965  areacirclem2  25983  areacirclem3  25984  areacirclem5  25987  areacirc  25989  nn0prpwlem  26017  filnetlem4  26102  isdmn3  26376  rmxycomplete  26672  gicabl  26933  lindfmm  26967  lindsmm  26968  lsslinds  26971  pm14.123b  27296  iotavalb  27300  climreeq  27408  frgra3vlem2  27755  trsbc  27969  bnj1280  28728  sbco2wAUX7  28921  sbco3wAUX7  28923  sbcomwAUX7  28924  sbal1NEW7  28949  sbalNEW7  28950  ax7w6AUX7  28985  sbco2OLD7  29069  sbco3OLD7  29071  sbcomOLD7  29072  sb9iOLD7  29075  sbcom2OLD7  29078  lcvp  29156  lcv2  29158  lsatnem0  29161  atnem0  29434  cvlsupr2  29459  cvr2N  29526  athgt  29571  2llnmat  29639  pmap11  29877  pmapeq0  29881  2lnat  29899  paddclN  29957  pmapjat1  29968  ltrn2ateq  30295  dihcnvord  31390  dihcnv11  31391  dih0bN  31397  dih0sb  31401  dihlspsnat  31449  dihatexv2  31455  dihglblem6  31456  dochvalr  31473  dochn0nv  31491  djhcvat42  31531  dochsatshp  31567  dochshpsat  31570  dochkrsat2  31572  lcfl5a  31613  lcfl8a  31619  lclkrlem2a  31623  mapdcnvordN  31774  hdmap14lem4a  31990  hgmapeq0  32023  hdmaplkr  32032  hdmapellkr  32033
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