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

Theorem bitr4d 259
Description: Deduction form of bitr4i 255. (Contributed by NM, 30-Jun-1993.)
Hypotheses
Ref Expression
bitr4d.1  |-  ( ph  ->  ( ps  <->  ch )
)
bitr4d.2  |-  ( ph  ->  ( th  <->  ch )
)
Assertion
Ref Expression
bitr4d  |-  ( ph  ->  ( ps  <->  th )
)

Proof of Theorem bitr4d
StepHypRef Expression
1 bitr4d.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
2 bitr4d.2 . . 3  |-  ( ph  ->  ( th  <->  ch )
)
32bicomd 204 . 2  |-  ( ph  ->  ( ch  <->  th )
)
41, 3bitrd 256 1  |-  ( ph  ->  ( ps  <->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187
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 188
This theorem is referenced by:  3bitr2d  284  3bitr2rd  285  3bitr4d  288  3bitr4rd  289  bianabs  888  3anibar  1173  sbcom3  2206  sbal1  2256  sbal2  2257  rmob2  3399  disjprg  4422  reuhypd  4649  opbrop  4934  opelresi  5136  ordsssuc  5528  iota1  5579  funbrfv2b  5925  dffn5  5926  dmfco  5955  fneqeql  6005  f1ompt  6059  dff13  6174  fliftcnv  6219  soisores  6233  isotr  6242  isoini  6244  caovord3  6496  releldm2  6857  brtpos  6990  tpostpos  7001  oe1m  7254  oawordri  7259  oalimcl  7269  omlimcl  7287  omabs  7356  iserd  7397  qliftel  7454  qliftfun  7456  qliftf  7459  ecopovsym  7473  pw2f1olem  7682  mapen  7742  suppeqfsuppbi  7903  funsnfsupp  7913  mapfien  7927  supisolem  7995  cantnflem1  8193  wemapwe  8201  rankr1clem  8290  rankr1c  8291  ranklim  8314  r1pwALT  8316  r1pwcl  8317  isfin1-2  8813  isfin1-4  8815  fin71num  8825  axdc3lem2  8879  ltmnq  9396  prlem936  9471  ltsosr  9517  ltasr  9523  xrlenlt  9698  ltxrlt  9703  letri3  9718  ne0gt0  9738  subadd  9877  ltsubadd2  10084  lesubadd2  10086  suble  10091  ltsub23  10093  ltaddpos2  10104  ltsubpos  10105  subge02  10129  ltord2  10142  leord2  10143  ltaddsublt  10238  divmul  10272  divmul3  10274  rec11r  10305  ltdiv1  10468  ltdivmul2  10481  ledivmul2  10483  ltrec  10487  ltdiv2  10491  negfi  10554  negiso  10587  infmrgelbOLD  10595  infmrlbOLD  10597  nnle1eq1  10637  avgle1  10852  avgle2  10853  avgle  10854  nn0le0eq0  10898  elz2  10954  znnnlt1  10964  zleltp1  10987  uzin  11191  difrp  11337  xrltlen  11445  dfle2  11446  xrletri3  11451  qbtwnre  11492  xltnegi  11509  supxrre  11613  supxrre1  11616  infxrre  11622  infmxrreOLD  11626  ixxun  11651  elioo5  11692  elfz5  11790  elfzm11  11863  uzsplit  11864  predfz  11912  flbi  12048  flbi2  12049  fznnfl  12086  zmodid2  12122  2submod  12148  lt2sq  12345  le2sq  12346  sqlecan  12378  bcval5  12500  shftfib  13114  mulre  13163  cnpart  13282  sqrlem6  13290  sqrmo  13294  elicc4abs  13361  abs2difabs  13376  cau4  13398  limsupgre  13520  limsupgreOLD  13521  clim2  13546  ello12  13558  ello1mpt2  13564  elo12  13569  lo1resb  13606  o1resb  13608  climeq  13609  climmpt2  13615  isercoll  13709  caucvgb  13724  fsumss  13769  fsumabs  13839  isumshft  13875  geomulcvg  13910  fprodss  13980  absefib  14230  dvdsval3  14287  dvdseq  14330  ndvdsadd  14364  bitscmp  14386  smupvallem  14431  dvdssq  14499  lcmdvds  14538  isprm3  14595  isprm5  14613  ncoprmgcdgt1b  14618  coprmdvds  14621  phiprmpw  14684  prmdiv  14693  pc11  14783  pcz  14784  pockthlem  14803  prmreclem2  14815  prmreclem4  14817  prmreclem6  14819  1arith  14825  vdwapun  14878  ramval  14914  ramvalOLD  14915  rami  14926  ramcl  14941  pwsle  15340  ercpbllem  15396  invsym  15609  funcres2c  15748  latnle  16273  grpinvcnv  16664  subgacs  16794  eqger  16809  gexdvds2  17163  pgpfi1  17173  pgpfi  17183  lsmass  17246  lssnle  17250  lsmdisj3b  17266  lsmhash  17281  ablsubadd  17380  gsumval3lem2  17466  subgdmdprd  17593  pgpfac1lem2  17634  dvdsr02  17810  drngid2  17917  issubrg3  17962  lssacs  18116  lspsnel5  18144  psrbaglefi  18522  coe1mul2lem1  18786  prmirred  18988  chrdvds  19021  chrcong  19022  chrnzr  19023  znleval  19047  znleval2  19048  cygznlem3  19062  frlmbas  19240  elfilspd  19283  lindfmm  19307  islindf4  19318  islindf5  19319  mdetunilem9  19567  discld  20027  isneip  20043  neiptopnei  20070  lpdifsn  20081  restopnb  20113  restopn2  20115  restdis  20116  restperf  20122  lmbr2  20197  cncls2  20211  cnprest  20227  cnprest2  20228  iscnrm2  20276  ist0-2  20282  cnt0  20284  ist1-3  20287  ishaus2  20289  cmpfi  20345  dfcon2  20356  1stccnp  20399  1stccn  20400  subislly  20418  hausmapdom  20437  kgencn  20493  tx1cn  20546  tx2cn  20547  txcnmpt  20561  txrest  20568  hauseqlcld  20583  tgqtop  20649  qtopcld  20650  qtopcn  20651  ordthmeolem  20738  trfil2  20824  trfil3  20825  trnei  20829  ufildr  20868  fmfg  20886  rnelfm  20890  fmfnfm  20895  elflim  20908  fbflim  20913  flimrest  20920  isflf  20930  cnflf  20939  cnflf2  20940  fclscf  20962  cnfcf  20979  ptcmplem2  20990  ghmcnp  21051  tsmssubm  21079  iscfilu  21225  xmetgt0  21295  prdsxmetlem  21305  elbl2ps  21326  elbl2  21327  blcomps  21330  blcom  21331  xblpnfps  21332  xblpnf  21333  blpnf  21334  xmeter  21370  setsxms  21416  imasf1obl  21425  stdbdbl  21454  metrest  21461  metcn  21480  txmetcn  21485  metuel2  21502  dscopn  21510  xrtgioo  21726  metdstri  21770  cncffvrn  21817  cnmpt2pc  21843  iihalf2  21848  icopnfhmeo  21858  evth2  21875  lmmbr3  22114  iscau3  22132  lmclimf  22157  metcld  22159  cfilucfil3  22172  srabn  22211  rrxmet  22246  minveclem4  22258  evthicc2  22283  ovolfioo  22290  ovolficc  22291  ovolgelb  22302  ovoliun  22327  shft2rab  22330  ovolshftlem1  22331  sca2rab  22334  ovolscalem1  22335  ismbl2  22349  ioombl1lem4  22382  mbfmulc2lem  22471  mbfmax  22473  mbfposr  22476  ismbf3d  22478  mbfaddlem  22484  mbfsup  22488  mbfinf  22489  mbfinfOLD  22490  i1f1lem  22515  i1fmulclem  22528  mbfi1fseqlem4  22544  itg2seq  22568  itg2monolem1  22576  itg2cnlem1  22587  itgfsum  22652  ditgneg  22680  limcdif  22699  limcnlp  22701  cnplimc  22710  rolle  22810  mvth  22812  dvne0  22831  lhop1lem  22833  itgsubst  22869  mdegle0  22894  deg1leb  22912  deg1le0  22928  q1peqb  22971  coemulhi  23067  dgrlt  23079  plydivlem3  23107  vieta1lem2  23123  aannenlem1  23140  ulmres  23199  reefiso  23259  pilem3  23265  pilem3OLD  23266  ellogdm  23440  root1eq1  23551  angpieqvdlem  23610  angpieqvdlem2  23611  quad2  23621  1cubr  23624  quart  23643  rlimcnp  23747  wilthlem2  23850  sgmss  23887  isppw  23895  dvdsflip  23965  dvdsflsumcom  23971  fsumvma  23995  logfac2  23999  chpchtsum  24001  dchrmulcl  24031  dchreq  24040  dchrresb  24041  bclbnd  24062  bposlem1  24066  bposlem5  24070  lgsneg  24101  lgsquadlem1  24136  lgsquadlem2  24137  m1lgs  24144  dchrisumlem3  24183  dchrisum0lem1  24208  trgcgrg  24413  tgellng  24449  lnrot1  24518  islnopp  24629  ismidb  24667  islmib  24676  ttgelitv  24750  axsegconlem6  24789  axeuclidlem  24829  axcontlem2  24832  axcontlem4  24834  axcontlem12  24842  dfconngra1  25235  clwwlkn2  25339  eupath2  25544  frgra3v  25566  drngoi  25971  nmoreltpnf  26246  isblo2  26260  nmlnogt0  26274  phoeqi  26335  ubthlem2  26349  hire  26573  normgt0  26606  ho01i  27307  ho02i  27308  hoeq1  27309  hoeq2  27310  nmopreltpnf  27348  adjeq  27414  leop  27602  leopmul2i  27614  pjnormssi  27647  pjimai  27655  jplem1  27747  mddmd2  27788  mdslmd1lem1  27804  mdslmd1lem2  27805  superpos  27833  atnssm0  27855  dmdbr5ati  27901  disjunsn  28034  fcoinvbr  28045  feqmptdf  28089  ofpreima  28099  funcnv5mpt  28103  isoun  28113  fpwrelmapffslem  28151  fpwrelmap  28152  xgepnf  28161  xlemnf  28162  xrge0infssd  28173  iocinioc2  28188  xrdifh  28189  nndiffz1  28193  xdivmul  28223  isarchi2  28331  smatrcl  28452  fimaproj  28490  sqsscirc2  28545  xrmulc1cn  28566  ismntoplly  28659  esumfsup  28721  esum2dlem  28743  1stmbfm  28912  2ndmbfm  28913  mbfmcnt  28920  oms0  28949  eulerpartlems  29010  eulerpartlemd  29016  ballotlemfc0  29142  ballotlemfcc  29143  ballotlemsima  29165  ballotlemfrcn0  29179  sgn3da  29191  bnj1173  29590  erdszelem7  29699  erdszelem9  29701  iscvm  29761  cvmlift3lem4  29824  sltval2  30321  fscgr  30623  seglelin  30659  btwnoutside  30668  lineunray  30690  cldbnd  30758  isfne4  30772  fneval  30784  filnetlem4  30813  nndivsub  30893  wl-sbhbt  31580  wl-sbcom2d  31589  wl-sbalnae  31590  wl-ax11-lem8  31616  sin2h  31629  cos2h  31630  ptrest  31633  poimirlem3  31637  poimirlem4  31638  poimirlem22  31656  poimirlem27  31661  mblfinlem3  31673  mblfinlem4  31674  ismblfin  31675  itg2addnclem  31687  itg2addnclem2  31688  itg2gt0cn  31691  iblabsnclem  31699  ftc1anclem6  31716  areacirclem2  31727  areacirclem5  31730  areacirc  31731  cover2  31734  mettrifi  31780  prter3  32152  islshpat  32282  lsatnle  32309  ellkr2  32356  lshpkr  32382  lkr0f2  32426  lduallkr3  32427  lkreqN  32435  cvrval2  32539  isat3  32572  glbconN  32641  hlrelat5N  32665  cvrval4N  32678  atlt  32701  1cvrco  32736  pmaple  33025  isline2  33038  isline4N  33041  elpaddn0  33064  elpadd2at2  33071  cdlemkid4  34200  dia0  34319  cdlemm10N  34385  dibglbN  34433  dihmeetlem4preN  34573  dochkrshp3  34655  dvh4dimlem  34710  lcfl5  34763  mapdpglem3  34942  mapdheq  34995  hdmap1eq  35069  hdmapval2lem  35101  hdmapoc  35201  hlhillcs  35228  fz1eqin  35310  diophin  35314  dvdsabsmod0OLD  35537  divalgmodcl  35538  jm2.19  35544  rmxdiophlem  35566  pw2f1ocnv  35588  wepwsolem  35596  gicabl  35653  sdrgacs  35756  idomodle  35759  isdomn3  35770  extoimad  36234  radcnvrat  36290  bcc0  36316  unima  37041  clim2f  37278  2reu4a  37991  dfdfat2  38013  funbrafv2b  38041  dfafn5a  38042  mod2eq1n2dvds  38105  iccpartgtprec  38114  dfeven2  38159  dfodd3  38160  pfxsuffeqwrdeq  38327  leaddsuble  38382  isfusgracl  38486  lindslinindimp2lem4  39004  snlindsntor  39014  regt1loggt0  39098  elbigo2  39114  elbigolo1  39119  fldivexpfllog2  39127  nnlog2ge0lt1  39128  blenpw2m1  39141
  Copyright terms: Public domain W3C validator