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  1942  sbco2  2135  sbco3  2137  sbcom  2138  sb9i  2143  sbcom2  2163  sbal1  2176  sbal  2177  csbiebt  3247  prsspwg  3915  prsspwgOLD  3916  copsex2t  4403  copsex2g  4404  ordtri2  4576  onmindif  4630  reusv2lem5  4687  onmindif2  4751  ordunisuc2  4783  dfom2  4806  fnssresb  5516  fcnvres  5579  funimass5  5806  fmptco  5860  cbvfo  5981  isocnv  6009  isoini  6017  isoselem  6020  ovmpt2dxf  6158  caovcanrd  6209  riota2df  6529  ordge1n0  6701  ondif2  6705  oa00  6761  odi  6781  oeoe  6801  eceqoveq  6968  omsucdomOLD  7261  isfinite2  7324  unfilem1  7330  fodomfib  7345  inficl  7388  dffi3  7394  ordiso2  7440  ordtypelem9  7451  cantnfle  7582  cantnf  7605  wemapwe  7610  rankr1a  7718  bnd2  7773  iscard  7818  domtri2  7832  nnsdomel  7833  cardaleph  7926  dfac12lem2  7980  cfss  8101  axcc3  8274  fodomb  8360  iundom2g  8371  inar1  8606  ltpiord  8720  ordpinq  8776  suplem2pr  8886  enreceq  8900  subeq0  9283  negcon1  9309  lesub  9463  ltsub13  9465  subge0  9497  mul0or  9618  div11  9660  divmuleq  9675  ltmuldiv2  9837  lemuldiv2  9846  nn1suc  9977  addltmul  10159  elnnnn0  10219  znn0sub  10279  prime  10306  uzindOLD  10320  zbtwnre  10528  xadddi2  10832  supxrbnd  10863  fz1n  11029  fzrev3  11067  modsubdir  11240  om2uzlt2i  11246  hashf1lem1  11659  cnpart  12000  sqr11  12023  sqrsq2  12029  absdiflt  12076  absdifle  12077  sqreulem  12118  sqreu  12119  eqsqror  12125  clim2  12253  climshft2  12331  isercoll  12416  sumrb  12462  supcvg  12590  sinbnd  12736  cosbnd  12737  sqr2irr  12803  dvdscmulr  12833  dvdsmulcr  12834  oddm1even  12864  bitsmod  12903  bitsinv1lem  12908  isprm3  13043  prmrp  13056  qredeq  13061  crt  13122  pcdvdsb  13197  pceq0  13199  unbenlem  13231  ramcl  13352  pwselbasb  13665  pwsle  13669  imasleval  13721  xpsfrnel2  13745  acsfn  13839  ismon2  13915  isepi2  13922  epii  13924  fthsect  14077  fthmon  14079  isipodrs  14542  ipodrsfi  14544  imasmnd2  14687  gsumval2a  14737  grpid  14795  grplmulf1o  14820  imasgrp2  14888  ghmeqker  14987  ghmf1  14989  gacan  15037  odmulgeq  15148  pgpssslw  15203  efgsfo  15326  efgred  15335  abladdsub4  15393  subgdmdprd  15547  imasrng  15680  lspsnss2  16036  gsumbagdiaglem  16395  znf1o  16787  znfld  16796  znunit  16799  znrrg  16801  iporthcom  16821  ip2eq  16839  obsne0  16907  eltg3  16982  eltop  16994  eltop2  16995  eltop3  16996  lmbrf  17278  cncnpi  17296  dfcon2  17435  1stcfb  17461  elptr  17558  xkoccn  17604  txcn  17611  hausdiag  17630  hmeoimaf1o  17755  isfbas  17814  ufileu  17904  alexsubALTlem4  18034  tsmsf1o  18127  ismet2  18316  imasdsf1olem  18356  imasf1oxmet  18358  imasf1omet  18359  xmseq0  18447  imasf1oxms  18472  metucnOLD  18571  metucn  18572  nrmmetd  18575  nlmmul0or  18672  xrsxmet  18793  metdseq0  18837  elpi1i  19024  cphsqrcl2  19102  tchcph  19147  lmmbrf  19168  caucfil  19189  lmclim  19208  cmsss  19256  srabn  19267  ovolfioo  19317  ovolficc  19318  elovolmr  19325  ovolctb  19339  ovolicc2lem3  19368  mbfmulc2lem  19492  mbfimaopnlem  19500  itg2mulclem  19591  iblrelem  19635  ellimc2  19717  mdegle0  19953  fta1glem2  20042  dgreq0  20136  plydivlem4  20166  plydivex  20167  fta1  20178  quotcan  20179  logeftb  20431  quad2  20632  cubic2  20641  dquartlem1  20644  atandm4  20672  fsumharmonic  20803  wilthlem1  20804  basellem8  20823  mumullem2  20916  chpchtsum  20956  logfaclbnd  20959  dchrelbas4  20980  lgsne0  21070  lgsqrlem2  21079  lgsdchrval  21084  lgsquadlem1  21091  lgsquadlem2  21092  2sqlem7  21107  dchrisum0lem1  21163  eupath2lem3  21654  grpoid  21764  grpodiveq  21797  nvsubadd  22089  nvmeq0  22098  nvgt0  22117  imsmetlem  22135  nmlnogt0  22251  ip2eqi  22311  hvaddcan2  22526  hvmulcan2  22528  hvaddsub4  22533  hi2eq  22560  pjhtheu  22849  lnopeqi  23464  riesz1  23521  jpi  23726  chcv2  23812  cvp  23831  atnemeq0  23833  fmptcof2  24029  funcnvmptOLD  24035  funcnvmpt  24036  xrge0addgt0  24167  lmlim  24286  ballotlemfc0  24703  ballotlemfcc  24704  ghomf1olem  25058  mulcan1g  25142  subeqrev  25150  fz0n  25155  prodrblem2  25210  imageval  25683  onsuct0  26095  onint1  26103  mblfinlem2  26144  ovoliunnfl  26147  voliunnfl  26149  volsupnfl  26150  mbfresfi  26152  mbfposadd  26153  itg2addnclem  26155  itg2addnclem2  26156  itg2addnc  26158  itg2gt0cn  26159  itgaddnclem2  26163  areacirclem2  26181  areacirclem3  26182  areacirclem5  26185  areacirc  26187  nn0prpwlem  26215  filnetlem4  26300  isdmn3  26574  rmxycomplete  26870  gicabl  27131  lindfmm  27165  lindsmm  27166  lsslinds  27169  pm14.123b  27494  iotavalb  27498  climreeq  27606  frgra3vlem2  28105  trsbc  28336  bnj1280  29095  sbco2wAUX7  29288  sbco3wAUX7  29290  sbcomwAUX7  29291  sbal1NEW7  29316  sbalNEW7  29317  ax7w6AUX7  29352  sbco2OLD7  29436  sbco3OLD7  29438  sbcomOLD7  29439  sb9iOLD7  29442  sbcom2OLD7  29445  lcvp  29523  lcv2  29525  lsatnem0  29528  atnem0  29801  cvlsupr2  29826  cvr2N  29893  athgt  29938  2llnmat  30006  pmap11  30244  pmapeq0  30248  2lnat  30266  paddclN  30324  pmapjat1  30335  ltrn2ateq  30662  dihcnvord  31757  dihcnv11  31758  dih0bN  31764  dih0sb  31768  dihlspsnat  31816  dihatexv2  31822  dihglblem6  31823  dochvalr  31840  dochn0nv  31858  djhcvat42  31898  dochsatshp  31934  dochshpsat  31937  dochkrsat2  31939  lcfl5a  31980  lcfl8a  31986  lclkrlem2a  31990  mapdcnvordN  32141  hdmap14lem4a  32357  hgmapeq0  32390  hdmaplkr  32399  hdmapellkr  32400
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