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  875  3anibar  1156  sbcom3  2105  sbal1  2171  sbal2  2173  disjprg  4309  reuhypd  4540  ordsssuc  4826  opbrop  4937  opelresi  5143  iota1  5416  funbrfv2b  5757  dffn5  5758  dmfco  5786  fneqeql  5832  f1ompt  5886  dff13  5992  fliftcnv  6025  soisores  6039  isotr  6048  isoini  6050  caovord3  6297  releldm2  6645  brtpos  6775  tpostpos  6786  oe1m  7005  oawordri  7010  oalimcl  7020  omlimcl  7038  omabs  7107  iserd  7148  qliftel  7204  qliftfun  7206  qliftf  7209  ecopovsym  7223  pw2f1olem  7436  mapen  7496  suppeqfsuppbi  7655  funsnfsupp  7665  mapfien  7678  supisolem  7741  wemapso2OLD  7787  cantnflem1  7918  cantnflem1OLD  7941  mapfienOLD  7948  wemapwe  7949  wemapweOLD  7950  rankr1clem  8048  rankr1c  8049  ranklim  8072  r1pwOLD  8074  r1pwcl  8075  isfin1-2  8575  isfin1-4  8577  fin71num  8587  axdc3lem2  8641  ltmnq  9162  prlem936  9237  ltsosr  9282  ltasr  9288  xrlenlt  9463  ltxrlt  9466  letri3  9481  ne0gt0  9500  subadd  9634  ltsubadd2  9831  lesubadd2  9833  suble  9838  ltsub23  9840  ltaddpos2  9851  ltsubpos  9852  subge02  9876  ltord2  9890  leord2  9891  ltaddsublt  9984  divmul  10018  divmul3  10020  rec11r  10051  ltdiv1  10214  ltdivmul2  10228  ledivmul2  10230  ltrec  10234  ltdiv2  10238  negiso  10327  infmrgelb  10331  infmrlb  10332  nnle1eq1  10371  avgle1  10585  avgle2  10586  avgle  10587  nn0le0eq0  10629  elz2  10684  znnnlt1  10694  zleltp1  10716  uzin  10914  difrp  11045  xrltlen  11144  dfle2  11145  xrletri3  11150  qbtwnre  11190  xltnegi  11207  supxrre  11311  supxrre1  11314  infmxrre  11319  ixxun  11337  elioo5  11374  elfz5  11466  elfzm11  11549  uzsplit  11551  flbi  11685  flbi2  11686  fznnfl  11722  zmodid2  11757  2submod  11781  lt2sq  11960  le2sq  11961  sqlecan  11993  bcval5  12115  shftfib  12582  mulre  12631  cnpart  12750  sqrlem6  12758  sqrmo  12762  elicc4abs  12828  abs2difabs  12843  cau4  12865  limsupgre  12980  clim2  13003  ello12  13015  ello1mpt2  13021  elo12  13026  lo1resb  13063  o1resb  13065  climeq  13066  climmpt2  13072  isercoll  13166  caucvgb  13178  fsumss  13223  fsumabs  13285  isumshft  13323  geomulcvg  13357  absefib  13503  xpnnenOLD  13513  dvdsval3  13560  dvdseq  13601  ndvdsadd  13633  bitscmp  13655  smupvallem  13700  dvdssq  13765  isprm3  13793  coprmdvds  13809  isprm5  13819  phiprmpw  13872  prmdiv  13881  pc11  13967  pcz  13968  pockthlem  13987  prmreclem2  13999  prmreclem4  14001  prmreclem6  14003  1arith  14009  vdwapun  14056  ramval  14090  rami  14097  ramcl  14111  pwsle  14451  ercpbllem  14507  invsym  14721  funcres2c  14832  latnle  15276  grpinvcnv  15615  subgacs  15737  eqger  15752  gexdvds2  16105  pgpfi1  16115  pgpfi  16125  lsmass  16188  lssnle  16192  lsmdisj3b  16208  lsmhash  16223  ablsubadd  16322  gsumval3OLD  16403  gsumval3lem2  16405  subgdmdprd  16553  pgpfac1lem2  16598  dvdsr02  16770  drngid2  16870  issubrg3  16915  lssacs  17070  lspsnel5  17098  psrbaglefi  17463  psrbaglefiOLD  17464  coe1mul2lem1  17743  prmirred  17941  prmirredOLD  17944  chrdvds  17981  chrcong  17982  chrnzr  17983  znleval  18009  znleval2  18010  cygznlem3  18024  frlmbas  18202  elfilspd  18254  lindfmm  18278  islindf4  18289  islindf5  18290  mdetunilem9  18448  discld  18715  isneip  18731  neiptopnei  18758  lpdifsn  18769  restopnb  18801  restopn2  18803  restdis  18804  restperf  18810  lmbr2  18885  cncls2  18899  cnprest  18915  cnprest2  18916  iscnrm2  18964  ist0-2  18970  cnt0  18972  ist1-3  18975  ishaus2  18977  cmpfi  19033  dfcon2  19045  1stccnp  19088  1stccn  19089  subislly  19107  hausmapdom  19126  kgencn  19151  tx1cn  19204  tx2cn  19205  txcnmpt  19219  txrest  19226  hauseqlcld  19241  tgqtop  19307  qtopcld  19308  qtopcn  19309  ordthmeolem  19396  trfil2  19482  trfil3  19483  trnei  19487  ufildr  19526  fmfg  19544  rnelfm  19548  fmfnfm  19553  elflim  19566  fbflim  19571  flimrest  19578  isflf  19588  cnflf  19597  cnflf2  19598  fclscf  19620  cnfcf  19637  ptcmplem2  19647  ghmcnp  19707  tsmssubm  19738  iscfilu  19885  xmetgt0  19955  prdsxmetlem  19965  elbl2ps  19986  elbl2  19987  blcomps  19990  blcom  19991  xblpnfps  19992  xblpnf  19993  blpnf  19994  xmeter  20030  setsxms  20076  imasf1obl  20085  stdbdbl  20114  metrest  20121  metcn  20140  txmetcn  20145  metuel2  20176  dscopn  20188  xrtgioo  20405  metdstri  20449  cncffvrn  20496  cnmpt2pc  20522  iihalf2  20527  icopnfhmeo  20537  evth2  20554  lmmbr3  20793  iscau3  20811  lmclimf  20836  metcld  20838  cfilucfil3OLD  20851  cfilucfil3  20852  srabn  20894  rrxmet  20929  minveclem4  20941  evthicc2  20966  ovolfioo  20973  ovolficc  20974  ovolgelb  20985  ovoliun  21010  shft2rab  21013  ovolshftlem1  21014  sca2rab  21017  ovolscalem1  21018  ismbl2  21032  ioombl1lem4  21064  mbfmulc2lem  21147  mbfmax  21149  mbfposr  21152  ismbf3d  21154  mbfaddlem  21160  mbfsup  21164  mbfinf  21165  i1f1lem  21189  i1fmulclem  21202  mbfi1fseqlem4  21218  itg2seq  21242  itg2monolem1  21250  itg2cnlem1  21261  itgfsum  21326  ditgneg  21354  limcdif  21373  limcnlp  21375  cnplimc  21384  rolle  21484  mvth  21486  dvne0  21505  lhop1lem  21507  itgsubst  21543  mdegle0  21570  deg1leb  21588  deg1le0  21605  q1peqb  21648  coemulhi  21743  dgrlt  21755  plydivlem3  21783  vieta1lem2  21799  aannenlem1  21816  ulmres  21875  reefiso  21935  pilem3  21940  ellogdm  22106  root1eq1  22215  angpieqvdlem  22245  angpieqvdlem2  22246  quad2  22256  1cubr  22259  quart  22278  rlimcnp  22381  wilthlem2  22429  sgmss  22466  isppw  22474  dvdsflip  22544  dvdsflsumcom  22550  fsumvma  22574  logfac2  22578  chpchtsum  22580  dchrmulcl  22610  dchreq  22619  dchrresb  22620  bclbnd  22641  bposlem1  22645  bposlem5  22649  lgsneg  22680  lgsquadlem1  22715  lgsquadlem2  22716  m1lgs  22723  dchrisumlem3  22762  dchrisum0lem1  22787  trgcgrg  22989  tgellng  23009  lnrot1  23052  ttgelitv  23151  axsegconlem6  23190  axeuclidlem  23230  axcontlem2  23233  axcontlem4  23235  axcontlem12  23243  dfconngra1  23579  eupath2  23623  drngoi  23916  nmoreltpnf  24191  isblo2  24205  nmlnogt0  24219  phoeqi  24280  ubthlem2  24294  hire  24518  normgt0  24551  ho01i  25254  ho02i  25255  hoeq1  25256  hoeq2  25257  nmopreltpnf  25295  adjeq  25361  leop  25549  leopmul2i  25561  pjnormssi  25594  pjimai  25602  jplem1  25694  mddmd2  25735  mdslmd1lem1  25751  mdslmd1lem2  25752  superpos  25780  atnssm0  25802  dmdbr5ati  25848  disjunsn  25958  feqmptdf  26000  ofpreima  26006  funcnv5mpt  26010  isoun  26019  fpwrelmapffslem  26054  fpwrelmap  26055  xgepnf  26065  xlemnf  26066  xrge0infssd  26076  iocinioc2  26091  xrdifh  26092  xdivmul  26122  isinftm  26220  isarchi2  26224  metidv  26341  pstmxmet  26346  sqsscirc2  26361  xrmulc1cn  26382  esumfsup  26541  1stmbfm  26697  2ndmbfm  26698  mbfmcnt  26705  oms0  26732  eulerpartlems  26765  eulerpartlemd  26771  ballotlemfc0  26897  ballotlemfcc  26898  ballotlemsima  26920  ballotlemfrcn0  26934  sgn3da  26946  erdszelem7  27107  erdszelem9  27109  iscvm  27170  cvmlift3lem4  27233  fprodss  27483  predfz  27686  sltval2  27819  fscgr  28133  seglelin  28169  btwnoutside  28178  lineunray  28200  nndivsub  28325  wl-sbhbt  28404  wl-sbcom2d  28413  wl-sbalnae  28414  wl-ax11-lem8  28434  sin2h  28448  cos2h  28449  ptrest  28451  mblfinlem3  28456  mblfinlem4  28457  ismblfin  28458  itg2addnclem  28469  itg2addnclem2  28470  itg2gt0cn  28473  iblabsnclem  28481  ftc1anclem6  28498  areacirclem2  28511  areacirclem5  28514  areacirc  28515  cldbnd  28547  isfne4  28567  fneval  28585  filnetlem4  28628  cover2  28633  mettrifi  28679  prter3  29053  fz1eqin  29133  diophin  29137  dvdsabsmod0  29361  divalgmodcl  29362  jm2.19  29368  rmxdiophlem  29390  pw2f1ocnv  29412  wepwsolem  29420  gicabl  29480  sdrgacs  29584  idomodle  29587  isdomn3  29598  2reu4a  30039  dfdfat2  30063  funbrafv2b  30091  dfafn5a  30092  leaddsuble  30200  clwwlkn2  30464  frgra3v  30620  lindslinindimp2lem4  30992  snlindsntor  31002  bnj1173  32089  islshpat  32758  lsatnle  32785  ellkr2  32832  lshpkr  32858  lkr0f2  32902  lduallkr3  32903  lkreqN  32911  cvrval2  33015  isat3  33048  glbconN  33117  hlrelat5N  33141  cvrval4N  33154  atlt  33177  1cvrco  33212  pmaple  33501  isline2  33514  isline4N  33517  elpaddn0  33540  elpadd2at2  33547  cdlemkid4  34674  dia0  34793  cdlemm10N  34859  dibglbN  34907  dihmeetlem4preN  35047  dochkrshp3  35129  dvh4dimlem  35184  lcfl5  35237  mapdpglem3  35416  mapdheq  35469  hdmap1eq  35543  hdmapval2lem  35575  hdmapoc  35675  hlhillcs  35702
  Copyright terms: Public domain W3C validator