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

Theorem bitr4d 256
Description: Deduction form of bitr4i 252. (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 201 . 2  |-  ( ph  ->  ( ch  <->  th )
)
41, 3bitrd 253 1  |-  ( ph  ->  ( ps  <->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
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 185
This theorem is referenced by:  3bitr2d  281  3bitr2rd  282  3bitr4d  285  3bitr4rd  286  bianabs  878  3anibar  1164  sbcom3  2128  sbal1  2193  sbal2  2195  rmob2  3433  disjprg  4443  reuhypd  4674  ordsssuc  4964  opbrop  5079  opelresi  5285  iota1  5565  funbrfv2b  5912  dffn5  5913  dmfco  5941  fneqeql  5989  f1ompt  6043  dff13  6154  fliftcnv  6197  soisores  6211  isotr  6220  isoini  6222  caovord3  6472  releldm2  6834  brtpos  6964  tpostpos  6975  oe1m  7194  oawordri  7199  oalimcl  7209  omlimcl  7227  omabs  7296  iserd  7337  qliftel  7394  qliftfun  7396  qliftf  7399  ecopovsym  7413  pw2f1olem  7621  mapen  7681  suppeqfsuppbi  7843  funsnfsupp  7853  mapfien  7867  supisolem  7931  wemapso2OLD  7977  cantnflem1  8108  cantnflem1OLD  8131  mapfienOLD  8138  wemapwe  8139  wemapweOLD  8140  rankr1clem  8238  rankr1c  8239  ranklim  8262  r1pwOLD  8264  r1pwcl  8265  isfin1-2  8765  isfin1-4  8767  fin71num  8777  axdc3lem2  8831  ltmnq  9350  prlem936  9425  ltsosr  9471  ltasr  9477  xrlenlt  9652  ltxrlt  9655  letri3  9670  ne0gt0  9689  subadd  9823  ltsubadd2  10023  lesubadd2  10025  suble  10030  ltsub23  10032  ltaddpos2  10043  ltsubpos  10044  subge02  10068  ltord2  10082  leord2  10083  ltaddsublt  10176  divmul  10210  divmul3  10212  rec11r  10243  ltdiv1  10406  ltdivmul2  10420  ledivmul2  10422  ltrec  10426  ltdiv2  10430  negiso  10519  infmrgelb  10523  infmrlb  10524  nnle1eq1  10564  avgle1  10778  avgle2  10779  avgle  10780  nn0le0eq0  10824  elz2  10881  znnnlt1  10891  zleltp1  10913  uzin  11114  difrp  11253  xrltlen  11352  dfle2  11353  xrletri3  11358  qbtwnre  11398  xltnegi  11415  supxrre  11519  supxrre1  11522  infmxrre  11527  ixxun  11545  elioo5  11582  elfz5  11680  elfzm11  11749  uzsplit  11750  flbi  11920  flbi2  11921  fznnfl  11957  zmodid2  11992  2submod  12016  lt2sq  12209  le2sq  12210  sqlecan  12242  bcval5  12364  shftfib  12868  mulre  12917  cnpart  13036  sqrlem6  13044  sqrmo  13048  elicc4abs  13115  abs2difabs  13130  cau4  13152  limsupgre  13267  clim2  13290  ello12  13302  ello1mpt2  13308  elo12  13313  lo1resb  13350  o1resb  13352  climeq  13353  climmpt2  13359  isercoll  13453  caucvgb  13465  fsumss  13510  fsumabs  13578  isumshft  13614  geomulcvg  13648  absefib  13794  xpnnenOLD  13804  dvdsval3  13851  dvdseq  13892  ndvdsadd  13925  bitscmp  13947  smupvallem  13992  dvdssq  14057  isprm3  14085  coprmdvds  14102  isprm5  14112  phiprmpw  14165  prmdiv  14174  pc11  14262  pcz  14263  pockthlem  14282  prmreclem2  14294  prmreclem4  14296  prmreclem6  14298  1arith  14304  vdwapun  14351  ramval  14385  rami  14392  ramcl  14406  pwsle  14747  ercpbllem  14803  invsym  15017  funcres2c  15128  latnle  15572  grpinvcnv  15916  subgacs  16041  eqger  16056  gexdvds2  16411  pgpfi1  16421  pgpfi  16431  lsmass  16494  lssnle  16498  lsmdisj3b  16514  lsmhash  16529  ablsubadd  16628  gsumval3OLD  16711  gsumval3lem2  16713  subgdmdprd  16883  pgpfac1lem2  16928  dvdsr02  17106  drngid2  17212  issubrg3  17257  lssacs  17413  lspsnel5  17441  psrbaglefi  17822  psrbaglefiOLD  17823  coe1mul2lem1  18107  prmirred  18320  prmirredOLD  18323  chrdvds  18360  chrcong  18361  chrnzr  18362  znleval  18388  znleval2  18389  cygznlem3  18403  frlmbas  18581  elfilspd  18633  lindfmm  18657  islindf4  18668  islindf5  18669  mdetunilem9  18917  discld  19384  isneip  19400  neiptopnei  19427  lpdifsn  19438  restopnb  19470  restopn2  19472  restdis  19473  restperf  19479  lmbr2  19554  cncls2  19568  cnprest  19584  cnprest2  19585  iscnrm2  19633  ist0-2  19639  cnt0  19641  ist1-3  19644  ishaus2  19646  cmpfi  19702  dfcon2  19714  1stccnp  19757  1stccn  19758  subislly  19776  hausmapdom  19795  kgencn  19820  tx1cn  19873  tx2cn  19874  txcnmpt  19888  txrest  19895  hauseqlcld  19910  tgqtop  19976  qtopcld  19977  qtopcn  19978  ordthmeolem  20065  trfil2  20151  trfil3  20152  trnei  20156  ufildr  20195  fmfg  20213  rnelfm  20217  fmfnfm  20222  elflim  20235  fbflim  20240  flimrest  20247  isflf  20257  cnflf  20266  cnflf2  20267  fclscf  20289  cnfcf  20306  ptcmplem2  20316  ghmcnp  20376  tsmssubm  20407  iscfilu  20554  xmetgt0  20624  prdsxmetlem  20634  elbl2ps  20655  elbl2  20656  blcomps  20659  blcom  20660  xblpnfps  20661  xblpnf  20662  blpnf  20663  xmeter  20699  setsxms  20745  imasf1obl  20754  stdbdbl  20783  metrest  20790  metcn  20809  txmetcn  20814  metuel2  20845  dscopn  20857  xrtgioo  21074  metdstri  21118  cncffvrn  21165  cnmpt2pc  21191  iihalf2  21196  icopnfhmeo  21206  evth2  21223  lmmbr3  21462  iscau3  21480  lmclimf  21505  metcld  21507  cfilucfil3OLD  21520  cfilucfil3  21521  srabn  21563  rrxmet  21598  minveclem4  21610  evthicc2  21635  ovolfioo  21642  ovolficc  21643  ovolgelb  21654  ovoliun  21679  shft2rab  21682  ovolshftlem1  21683  sca2rab  21686  ovolscalem1  21687  ismbl2  21701  ioombl1lem4  21734  mbfmulc2lem  21817  mbfmax  21819  mbfposr  21822  ismbf3d  21824  mbfaddlem  21830  mbfsup  21834  mbfinf  21835  i1f1lem  21859  i1fmulclem  21872  mbfi1fseqlem4  21888  itg2seq  21912  itg2monolem1  21920  itg2cnlem1  21931  itgfsum  21996  ditgneg  22024  limcdif  22043  limcnlp  22045  cnplimc  22054  rolle  22154  mvth  22156  dvne0  22175  lhop1lem  22177  itgsubst  22213  mdegle0  22240  deg1leb  22258  deg1le0  22275  q1peqb  22318  coemulhi  22413  dgrlt  22425  plydivlem3  22453  vieta1lem2  22469  aannenlem1  22486  ulmres  22545  reefiso  22605  pilem3  22610  ellogdm  22776  root1eq1  22885  angpieqvdlem  22915  angpieqvdlem2  22916  quad2  22926  1cubr  22929  quart  22948  rlimcnp  23051  wilthlem2  23099  sgmss  23136  isppw  23144  dvdsflip  23214  dvdsflsumcom  23220  fsumvma  23244  logfac2  23248  chpchtsum  23250  dchrmulcl  23280  dchreq  23289  dchrresb  23290  bclbnd  23311  bposlem1  23315  bposlem5  23319  lgsneg  23350  lgsquadlem1  23385  lgsquadlem2  23386  m1lgs  23393  dchrisumlem3  23432  dchrisum0lem1  23457  trgcgrg  23662  tgellng  23696  lnrot1  23745  ismidb  23849  islmib  23858  ttgelitv  23890  axsegconlem6  23929  axeuclidlem  23969  axcontlem2  23972  axcontlem4  23974  axcontlem12  23982  dfconngra1  24375  clwwlkn2  24479  eupath2  24684  frgra3v  24706  drngoi  25113  nmoreltpnf  25388  isblo2  25402  nmlnogt0  25416  phoeqi  25477  ubthlem2  25491  hire  25715  normgt0  25748  ho01i  26451  ho02i  26452  hoeq1  26453  hoeq2  26454  nmopreltpnf  26492  adjeq  26558  leop  26746  leopmul2i  26758  pjnormssi  26791  pjimai  26799  jplem1  26891  mddmd2  26932  mdslmd1lem1  26948  mdslmd1lem2  26949  superpos  26977  atnssm0  26999  dmdbr5ati  27045  disjunsn  27154  fcoinvbr  27162  feqmptdf  27201  ofpreima  27207  funcnv5mpt  27211  isoun  27220  fpwrelmapffslem  27255  fpwrelmap  27256  xgepnf  27266  xlemnf  27267  xrge0infssd  27277  iocinioc2  27286  xrdifh  27287  xdivmul  27317  isinftm  27415  isarchi2  27419  fimaproj  27527  metidv  27535  pstmxmet  27540  sqsscirc2  27555  xrmulc1cn  27576  ismntoplly  27671  esumfsup  27744  1stmbfm  27899  2ndmbfm  27900  mbfmcnt  27907  oms0  27934  eulerpartlems  27967  eulerpartlemd  27973  ballotlemfc0  28099  ballotlemfcc  28100  ballotlemsima  28122  ballotlemfrcn0  28136  sgn3da  28148  erdszelem7  28309  erdszelem9  28311  iscvm  28372  cvmlift3lem4  28435  fprodss  28685  predfz  28888  sltval2  29021  fscgr  29335  seglelin  29371  btwnoutside  29380  lineunray  29402  nndivsub  29527  wl-sbhbt  29607  wl-sbcom2d  29616  wl-sbalnae  29617  wl-ax11-lem8  29637  sin2h  29650  cos2h  29651  ptrest  29653  mblfinlem3  29658  mblfinlem4  29659  ismblfin  29660  itg2addnclem  29671  itg2addnclem2  29672  itg2gt0cn  29675  iblabsnclem  29683  ftc1anclem6  29700  areacirclem2  29713  areacirclem5  29716  areacirc  29717  cldbnd  29749  isfne4  29769  fneval  29787  filnetlem4  29830  cover2  29835  mettrifi  29881  prter3  30255  fz1eqin  30334  diophin  30338  dvdsabsmod0  30560  divalgmodcl  30561  jm2.19  30567  rmxdiophlem  30589  pw2f1ocnv  30611  wepwsolem  30619  gicabl  30679  sdrgacs  30783  idomodle  30786  isdomn3  30797  lcmdvds  30842  unima  31047  clim2f  31206  2reu4a  31689  dfdfat2  31711  funbrafv2b  31739  dfafn5a  31740  leaddsuble  31814  isfusgracl  31921  lindslinindimp2lem4  32161  snlindsntor  32171  bnj1173  33155  islshpat  33832  lsatnle  33859  ellkr2  33906  lshpkr  33932  lkr0f2  33976  lduallkr3  33977  lkreqN  33985  cvrval2  34089  isat3  34122  glbconN  34191  hlrelat5N  34215  cvrval4N  34228  atlt  34251  1cvrco  34286  pmaple  34575  isline2  34588  isline4N  34591  elpaddn0  34614  elpadd2at2  34621  cdlemkid4  35748  dia0  35867  cdlemm10N  35933  dibglbN  35981  dihmeetlem4preN  36121  dochkrshp3  36203  dvh4dimlem  36258  lcfl5  36311  mapdpglem3  36490  mapdheq  36543  hdmap1eq  36617  hdmapval2lem  36649  hdmapoc  36749  hlhillcs  36776
  Copyright terms: Public domain W3C validator