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, 5-Aug-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  868  3anibar  1149  sbcom3  2106  sbal1  2173  sbal2  2175  disjprg  4276  reuhypd  4507  ordsssuc  4792  opbrop  4903  opelresiOLD  5109  opelresi  5110  iota1  5383  funbrfv2b  5724  dffn5  5725  dmfco  5753  fneqeql  5799  f1ompt  5853  dff13  5958  fliftcnv  5991  soisores  6005  isotr  6014  isoini  6016  caovord3  6265  releldm2  6613  brtpos  6743  tpostpos  6754  oe1m  6972  oawordri  6977  oalimcl  6987  omlimcl  7005  omabs  7074  iserd  7115  qliftel  7171  qliftfun  7173  qliftf  7176  ecopovsym  7190  pw2f1olem  7403  mapen  7463  suppeqfsuppbi  7622  funsnfsupp  7632  mapfien  7645  supisolem  7708  wemapso2OLD  7754  cantnflem1  7885  cantnflem1OLD  7908  mapfienOLD  7915  wemapwe  7916  wemapweOLD  7917  rankr1clem  8015  rankr1c  8016  ranklim  8039  r1pwOLD  8041  r1pwcl  8042  isfin1-2  8542  isfin1-4  8544  fin71num  8554  axdc3lem2  8608  ltmnq  9128  prlem936  9203  ltsosr  9248  ltasr  9254  xrlenlt  9429  ltxrlt  9432  letri3  9447  ne0gt0  9466  subadd  9600  ltsubadd2  9797  lesubadd2  9799  suble  9804  ltsub23  9806  ltaddpos2  9817  ltsubpos  9818  subge02  9842  ltord2  9856  leord2  9857  ltaddsublt  9950  divmul  9984  divmul3  9986  rec11r  10017  ltdiv1  10180  ltdivmul2  10194  ledivmul2  10196  ltrec  10200  ltdiv2  10204  negiso  10293  infmrgelb  10297  infmrlb  10298  nnle1eq1  10337  avgle1  10551  avgle2  10552  avgle  10553  nn0le0eq0  10595  elz2  10650  znnnlt1  10660  zleltp1  10682  uzin  10880  difrp  11011  xrltlen  11110  dfle2  11111  xrletri3  11116  qbtwnre  11156  xltnegi  11173  supxrre  11277  supxrre1  11280  infmxrre  11285  ixxun  11303  elioo5  11340  elfz5  11431  elfzm11  11511  uzsplit  11513  flbi  11647  flbi2  11648  fznnfl  11684  zmodid2  11719  2submod  11743  lt2sq  11922  le2sq  11923  sqlecan  11955  bcval5  12077  shftfib  12544  mulre  12593  cnpart  12712  sqrlem6  12720  sqrmo  12724  elicc4abs  12790  abs2difabs  12805  cau4  12827  limsupgre  12942  clim2  12965  ello12  12977  ello1mpt2  12983  elo12  12988  lo1resb  13025  o1resb  13027  climeq  13028  climmpt2  13034  isercoll  13128  caucvgb  13140  fsumss  13185  fsumabs  13246  isumshft  13284  geomulcvg  13318  absefib  13464  xpnnenOLD  13474  dvdsval3  13521  dvdseq  13562  ndvdsadd  13594  bitscmp  13616  smupvallem  13661  dvdssq  13726  isprm3  13754  coprmdvds  13770  isprm5  13780  phiprmpw  13833  prmdiv  13842  pc11  13928  pcz  13929  pockthlem  13948  prmreclem2  13960  prmreclem4  13962  prmreclem6  13964  1arith  13970  vdwapun  14017  ramval  14051  rami  14058  ramcl  14072  pwsle  14412  ercpbllem  14468  invsym  14682  funcres2c  14793  latnle  15237  grpinvcnv  15573  subgacs  15695  eqger  15710  gexdvds2  16063  pgpfi1  16073  pgpfi  16083  lsmass  16146  lssnle  16150  lsmdisj3b  16166  lsmhash  16181  ablsubadd  16280  gsumval3OLD  16361  gsumval3lem2  16363  subgdmdprd  16504  pgpfac1lem2  16549  dvdsr02  16681  drngid2  16771  issubrg3  16816  lssacs  16969  lspsnel5  16997  psrbaglefi  17374  psrbaglefiOLD  17375  coe1mul2lem1  17618  prmirred  17760  prmirredOLD  17763  chrdvds  17800  chrcong  17801  chrnzr  17802  znleval  17828  znleval2  17829  cygznlem3  17843  frlmbas  18021  elfilspd  18073  lindfmm  18097  islindf4  18108  islindf5  18109  mdetunilem9  18267  discld  18534  isneip  18550  neiptopnei  18577  lpdifsn  18588  restopnb  18620  restopn2  18622  restdis  18623  restperf  18629  lmbr2  18704  cncls2  18718  cnprest  18734  cnprest2  18735  iscnrm2  18783  ist0-2  18789  cnt0  18791  ist1-3  18794  ishaus2  18796  cmpfi  18852  dfcon2  18864  1stccnp  18907  1stccn  18908  subislly  18926  hausmapdom  18945  kgencn  18970  tx1cn  19023  tx2cn  19024  txcnmpt  19038  txrest  19045  hauseqlcld  19060  tgqtop  19126  qtopcld  19127  qtopcn  19128  ordthmeolem  19215  trfil2  19301  trfil3  19302  trnei  19306  ufildr  19345  fmfg  19363  rnelfm  19367  fmfnfm  19372  elflim  19385  fbflim  19390  flimrest  19397  isflf  19407  cnflf  19416  cnflf2  19417  fclscf  19439  cnfcf  19456  ptcmplem2  19466  ghmcnp  19526  tsmssubm  19557  iscfilu  19704  xmetgt0  19774  prdsxmetlem  19784  elbl2ps  19805  elbl2  19806  blcomps  19809  blcom  19810  xblpnfps  19811  xblpnf  19812  blpnf  19813  xmeter  19849  setsxms  19895  imasf1obl  19904  stdbdbl  19933  metrest  19940  metcn  19959  txmetcn  19964  metuel2  19995  dscopn  20007  xrtgioo  20224  metdstri  20268  cncffvrn  20315  cnmpt2pc  20341  iihalf2  20346  icopnfhmeo  20356  evth2  20373  lmmbr3  20612  iscau3  20630  lmclimf  20655  metcld  20657  cfilucfil3OLD  20670  cfilucfil3  20671  srabn  20713  rrxmet  20748  minveclem4  20760  evthicc2  20785  ovolfioo  20792  ovolficc  20793  ovolgelb  20804  ovoliun  20829  shft2rab  20832  ovolshftlem1  20833  sca2rab  20836  ovolscalem1  20837  ismbl2  20851  ioombl1lem4  20883  mbfmulc2lem  20966  mbfmax  20968  mbfposr  20971  ismbf3d  20973  mbfaddlem  20979  mbfsup  20983  mbfinf  20984  i1f1lem  21008  i1fmulclem  21021  mbfi1fseqlem4  21037  itg2seq  21061  itg2monolem1  21069  itg2cnlem1  21080  itgfsum  21145  ditgneg  21173  limcdif  21192  limcnlp  21194  cnplimc  21203  rolle  21303  mvth  21305  dvne0  21324  lhop1lem  21326  itgsubst  21362  mdegle0  21432  deg1leb  21450  deg1le0  21467  q1peqb  21510  coemulhi  21605  dgrlt  21617  plydivlem3  21645  vieta1lem2  21661  aannenlem1  21678  ulmres  21737  reefiso  21797  pilem3  21802  ellogdm  21968  root1eq1  22077  angpieqvdlem  22107  angpieqvdlem2  22108  quad2  22118  1cubr  22121  quart  22140  rlimcnp  22243  wilthlem2  22291  sgmss  22328  isppw  22336  dvdsflip  22406  dvdsflsumcom  22412  fsumvma  22436  logfac2  22440  chpchtsum  22442  dchrmulcl  22472  dchreq  22481  dchrresb  22482  bclbnd  22503  bposlem1  22507  bposlem5  22511  lgsneg  22542  lgsquadlem1  22577  lgsquadlem2  22578  m1lgs  22585  dchrisumlem3  22624  dchrisum0lem1  22649  trgcgrg  22847  tgellng  22865  lnrot1  22903  ttgelitv  22951  axsegconlem6  22990  axeuclidlem  23030  axcontlem2  23033  axcontlem4  23035  axcontlem12  23043  dfconngra1  23379  eupath2  23423  drngoi  23716  nmoreltpnf  23991  isblo2  24005  nmlnogt0  24019  phoeqi  24080  ubthlem2  24094  hire  24318  normgt0  24351  ho01i  25054  ho02i  25055  hoeq1  25056  hoeq2  25057  nmopreltpnf  25095  adjeq  25161  leop  25349  leopmul2i  25361  pjnormssi  25394  pjimai  25402  jplem1  25494  mddmd2  25535  mdslmd1lem1  25551  mdslmd1lem2  25552  superpos  25580  atnssm0  25602  dmdbr5ati  25648  disjunsn  25759  feqmptdf  25801  ofpreima  25807  funcnv5mpt  25811  isoun  25820  fpwrelmapffslem  25856  fpwrelmap  25857  xgepnf  25867  xlemnf  25868  iocinioc2  25891  xrdifh  25892  xdivmul  25922  isinftm  26021  isarchi2  26025  metidv  26172  pstmxmet  26177  sqsscirc2  26192  xrmulc1cn  26213  esumfsup  26372  1stmbfm  26528  2ndmbfm  26529  mbfmcnt  26536  eulerpartlems  26590  eulerpartlemd  26596  ballotlemfc0  26722  ballotlemfcc  26723  ballotlemsima  26745  ballotlemfrcn0  26759  sgn3da  26771  erdszelem7  26932  erdszelem9  26934  iscvm  26995  cvmlift3lem4  27058  fprodss  27307  predfz  27510  sltval2  27643  fscgr  27957  seglelin  27993  btwnoutside  28002  lineunray  28024  nndivsub  28150  wl-sbhbt  28224  wl-sbcom2d  28233  wl-sbalnae  28234  wl-ax11-lem8  28249  sin2h  28263  cos2h  28264  ptrest  28266  mblfinlem3  28271  mblfinlem4  28272  ismblfin  28273  itg2addnclem  28284  itg2addnclem2  28285  itg2gt0cn  28288  iblabsnclem  28296  ftc1anclem6  28313  areacirclem2  28326  areacirclem5  28329  areacirc  28330  cldbnd  28362  isfne4  28382  fneval  28400  filnetlem4  28443  cover2  28448  mettrifi  28494  prter3  28869  fz1eqin  28949  diophin  28953  dvdsabsmod0  29177  divalgmodcl  29178  jm2.19  29184  rmxdiophlem  29206  pw2f1ocnv  29228  wepwsolem  29236  gicabl  29296  sdrgacs  29400  idomodle  29403  isdomn3  29414  2reu4a  29856  dfdfat2  29880  funbrafv2b  29908  dfafn5a  29909  leaddsuble  30017  clwwlkn2  30281  frgra3v  30437  lindslinindimp2lem4  30701  snlindsntor  30711  bnj1173  31692  islshpat  32232  lsatnle  32259  ellkr2  32306  lshpkr  32332  lkr0f2  32376  lduallkr3  32377  lkreqN  32385  cvrval2  32489  isat3  32522  glbconN  32591  hlrelat5N  32615  cvrval4N  32628  atlt  32651  1cvrco  32686  pmaple  32975  isline2  32988  isline4N  32991  elpaddn0  33014  elpadd2at2  33021  cdlemkid4  34148  dia0  34267  cdlemm10N  34333  dibglbN  34381  dihmeetlem4preN  34521  dochkrshp3  34603  dvh4dimlem  34658  lcfl5  34711  mapdpglem3  34890  mapdheq  34943  hdmap1eq  35017  hdmapval2lem  35049  hdmapoc  35149  hlhillcs  35176
  Copyright terms: Public domain W3C validator