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

Theorem bitr4d 264
Description: Deduction form of bitr4i 260. (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 206 . 2  |-  ( ph  ->  ( ch  <->  th )
)
41, 3bitrd 261 1  |-  ( ph  ->  ( ps  <->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189
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 190
This theorem is referenced by:  3bitr2d  289  3bitr2rd  290  3bitr4d  293  3bitr4rd  294  bianabs  896  3anibar  1182  sbcom3  2251  sbal1  2300  sbal2  2301  rmob2  3373  disjprg  4412  reuhypd  4641  opbrop  4933  opelresi  5135  ordsssuc  5528  iota1  5579  funbrfv2b  5932  dffn5  5933  dmfco  5962  fneqeql  6013  f1ompt  6067  dff13  6184  fliftcnv  6229  soisores  6243  isotr  6252  isoini  6254  caovord3  6509  releldm2  6870  brtpos  7008  tpostpos  7019  oe1m  7272  oawordri  7277  oalimcl  7287  omlimcl  7305  omabs  7374  iserd  7415  qliftel  7472  qliftfun  7474  qliftf  7477  ecopovsym  7491  pw2f1olem  7702  mapen  7762  suppeqfsuppbi  7923  funsnfsupp  7933  mapfien  7947  supisolem  8015  cantnflem1  8220  wemapwe  8228  rankr1clem  8317  rankr1c  8318  ranklim  8341  r1pwALT  8343  r1pwcl  8344  isfin1-2  8841  isfin1-4  8843  fin71num  8853  axdc3lem2  8907  ltmnq  9423  prlem936  9498  ltsosr  9544  ltasr  9550  xrlenlt  9725  ltxrlt  9730  letri3  9745  ne0gt0  9765  subadd  9904  ltsubadd2  10113  lesubadd2  10115  suble  10120  ltsub23  10122  ltaddpos2  10133  ltsubpos  10134  subge02  10158  ltord2  10171  leord2  10172  ltaddsublt  10267  divmul  10301  divmul3  10303  rec11r  10334  ltdiv1  10497  ltdivmul2  10510  ledivmul2  10512  ltrec  10516  ltdiv2  10520  negfi  10582  negiso  10615  infmrgelbOLD  10623  infmrlbOLD  10625  nnle1eq1  10665  avgle1  10881  avgle2  10882  avgle  10883  nn0le0eq0  10927  elz2  10983  znnnlt1  10993  zleltp1  11016  uzin  11220  difrp  11366  xrltlen  11474  dfle2  11475  xrletri3  11480  qbtwnre  11521  xltnegi  11538  supxrre  11642  supxrre1  11645  infxrre  11651  infmxrreOLD  11655  ixxun  11680  elioo5  11721  elfz5  11821  elfzm11  11894  uzsplit  11895  predfz  11945  flbi  12083  flbi2  12084  fznnfl  12121  zmodid2  12157  2submod  12183  lt2sq  12380  le2sq  12381  sqlecan  12413  bcval5  12535  shftfib  13184  mulre  13233  cnpart  13352  sqrlem6  13360  sqrmo  13364  elicc4abs  13431  abs2difabs  13446  cau4  13468  limsupgre  13591  limsupgreOLD  13592  clim2  13617  ello12  13629  ello1mpt2  13635  elo12  13640  lo1resb  13677  o1resb  13679  climeq  13680  climmpt2  13686  isercoll  13780  caucvgb  13795  fsumss  13840  fsumabs  13910  isumshft  13946  geomulcvg  13981  fprodss  14051  absefib  14301  dvdsval3  14358  dvdseq  14401  ndvdsadd  14438  bitscmp  14461  smupvallem  14506  dvdssq  14577  lcmdvds  14622  isprm3  14682  isprm5  14700  ncoprmgcdgt1b  14705  coprmdvds  14708  phiprmpw  14773  prmdiv  14782  pc11  14878  pcz  14879  pockthlem  14898  prmreclem2  14910  prmreclem4  14912  prmreclem6  14914  1arith  14920  vdwapun  14973  ramval  15009  ramvalOLD  15010  rami  15021  ramcl  15036  pwsle  15439  ercpbllem  15503  invsym  15716  funcres2c  15855  latnle  16380  grpinvcnv  16771  subgacs  16901  eqger  16916  gexdvds2  17286  pgpfi1  17296  pgpfi  17306  lsmass  17369  lssnle  17373  lsmdisj3b  17389  lsmhash  17404  ablsubadd  17503  gsumval3lem2  17589  subgdmdprd  17716  pgpfac1lem2  17757  dvdsr02  17933  drngid2  18040  issubrg3  18085  lssacs  18239  lspsnel5  18267  psrbaglefi  18645  coe1mul2lem1  18909  prmirred  19115  chrdvds  19148  chrcong  19149  chrnzr  19150  znleval  19174  znleval2  19175  cygznlem3  19189  frlmbas  19367  elfilspd  19410  lindfmm  19434  islindf4  19445  islindf5  19446  mdetunilem9  19694  discld  20154  isneip  20170  neiptopnei  20197  lpdifsn  20208  restopnb  20240  restopn2  20242  restdis  20243  restperf  20249  lmbr2  20324  cncls2  20338  cnprest  20354  cnprest2  20355  iscnrm2  20403  ist0-2  20409  cnt0  20411  ist1-3  20414  ishaus2  20416  cmpfi  20472  dfcon2  20483  1stccnp  20526  1stccn  20527  subislly  20545  hausmapdom  20564  kgencn  20620  tx1cn  20673  tx2cn  20674  txcnmpt  20688  txrest  20695  hauseqlcld  20710  tgqtop  20776  qtopcld  20777  qtopcn  20778  ordthmeolem  20865  trfil2  20951  trfil3  20952  trnei  20956  ufildr  20995  fmfg  21013  rnelfm  21017  fmfnfm  21022  elflim  21035  fbflim  21040  flimrest  21047  isflf  21057  cnflf  21066  cnflf2  21067  fclscf  21089  cnfcf  21106  ptcmplem2  21117  ghmcnp  21178  tsmssubm  21206  iscfilu  21352  xmetgt0  21422  prdsxmetlem  21432  elbl2ps  21453  elbl2  21454  blcomps  21457  blcom  21458  xblpnfps  21459  xblpnf  21460  blpnf  21461  xmeter  21497  setsxms  21543  imasf1obl  21552  stdbdbl  21581  metrest  21588  metcn  21607  txmetcn  21612  metuel2  21629  dscopn  21637  xrtgioo  21873  metdstri  21917  metdstriOLD  21932  cncffvrn  21979  cnmpt2pc  22005  iihalf2  22010  icopnfhmeo  22020  evth2  22037  lmmbr3  22279  iscau3  22297  lmclimf  22322  metcld  22324  cfilucfil3  22337  srabn  22376  rrxmet  22411  minveclem4  22423  minveclem4OLD  22435  evthicc2  22460  ovolfioo  22469  ovolficc  22470  ovolgelb  22482  ovoliun  22507  shft2rab  22510  ovolshftlem1  22511  sca2rab  22514  ovolscalem1  22515  ismbl2  22530  ioombl1lem4  22563  mbfmulc2lem  22652  mbfmax  22654  mbfposr  22657  ismbf3d  22659  mbfaddlem  22665  mbfsup  22669  mbfinf  22670  mbfinfOLD  22671  i1f1lem  22696  i1fmulclem  22709  mbfi1fseqlem4  22725  itg2seq  22749  itg2monolem1  22757  itg2cnlem1  22768  itgfsum  22833  ditgneg  22861  limcdif  22880  limcnlp  22882  cnplimc  22891  rolle  22991  mvth  22993  dvne0  23012  lhop1lem  23014  itgsubst  23050  mdegle0  23075  deg1leb  23093  deg1le0  23109  q1peqb  23154  coemulhi  23257  dgrlt  23269  plydivlem3  23297  vieta1lem2  23313  aannenlem1  23333  ulmres  23392  reefiso  23452  pilem3  23458  pilem3OLD  23459  ellogdm  23633  root1eq1  23744  angpieqvdlem  23803  angpieqvdlem2  23804  quad2  23814  1cubr  23817  quart  23836  rlimcnp  23940  wilthlem2  24043  sgmss  24082  isppw  24090  dvdsflip  24160  dvdsflsumcom  24166  fsumvma  24190  logfac2  24194  chpchtsum  24196  dchrmulcl  24226  dchreq  24235  dchrresb  24236  bclbnd  24257  bposlem1  24261  bposlem5  24265  lgsneg  24296  lgsquadlem1  24331  lgsquadlem2  24332  m1lgs  24339  dchrisumlem3  24378  dchrisum0lem1  24403  trgcgrg  24609  tgellng  24647  lnrot1  24717  islnopp  24830  ismidb  24869  islmib  24878  isleag  24932  ttgelitv  24962  axsegconlem6  25001  axeuclidlem  25041  axcontlem2  25044  axcontlem4  25046  axcontlem12  25054  dfconngra1  25448  clwwlkn2  25552  eupath2  25757  frgra3v  25779  drngoi  26184  nmoreltpnf  26459  isblo2  26473  nmlnogt0  26487  phoeqi  26548  ubthlem2  26562  hire  26796  normgt0  26829  ho01i  27530  ho02i  27531  hoeq1  27532  hoeq2  27533  nmopreltpnf  27571  adjeq  27637  leop  27825  leopmul2i  27837  pjnormssi  27870  pjimai  27878  jplem1  27970  mddmd2  28011  mdslmd1lem1  28027  mdslmd1lem2  28028  superpos  28056  atnssm0  28078  dmdbr5ati  28124  disjunsn  28253  fcoinvbr  28264  feqmptdf  28307  ofpreima  28317  funcnv5mpt  28321  isoun  28331  fpwrelmapffslem  28366  fpwrelmap  28367  xgepnf  28376  xlemnf  28377  xrge0infssdOLD  28392  iocinioc2  28410  xrdifh  28411  nndiffz1  28415  xdivmul  28443  isarchi2  28551  smatrcl  28671  fimaproj  28709  sqsscirc2  28764  xrmulc1cn  28785  ismntoplly  28878  esumfsup  28940  esum2dlem  28962  1stmbfm  29131  2ndmbfm  29132  mbfmcnt  29139  oms0OLD  29178  eulerpartlems  29242  eulerpartlemd  29248  ballotlemfc0  29374  ballotlemfcc  29375  ballotlemsima  29397  ballotlemfrcn0  29411  ballotlemsimaOLD  29435  ballotlemfrcn0OLD  29449  sgn3da  29461  bnj1173  29860  erdszelem7  29969  erdszelem9  29971  iscvm  30031  cvmlift3lem4  30094  sltval2  30592  fscgr  30896  seglelin  30932  btwnoutside  30941  lineunray  30963  cldbnd  31031  isfne4  31045  fneval  31057  filnetlem4  31086  nndivsub  31166  wl-sbhbt  31927  wl-sbcom2d  31936  wl-sbalnae  31937  wl-ax11-lem8  31967  sin2h  31980  cos2h  31981  ptrest  31984  poimirlem3  31988  poimirlem4  31989  poimirlem22  32007  poimirlem27  32012  mblfinlem3  32024  mblfinlem4  32025  ismblfin  32026  itg2addnclem  32038  itg2addnclem2  32039  itg2gt0cn  32042  iblabsnclem  32050  ftc1anclem6  32067  areacirclem2  32078  areacirclem5  32081  areacirc  32082  cover2  32085  mettrifi  32131  prter3  32499  islshpat  32628  lsatnle  32655  ellkr2  32702  lshpkr  32728  lkr0f2  32772  lduallkr3  32773  lkreqN  32781  cvrval2  32885  isat3  32918  glbconN  32987  hlrelat5N  33011  cvrval4N  33024  atlt  33047  1cvrco  33082  pmaple  33371  isline2  33384  isline4N  33387  elpaddn0  33410  elpadd2at2  33417  cdlemkid4  34546  dia0  34665  cdlemm10N  34731  dibglbN  34779  dihmeetlem4preN  34919  dochkrshp3  35001  dvh4dimlem  35056  lcfl5  35109  mapdpglem3  35288  mapdheq  35341  hdmap1eq  35415  hdmapval2lem  35447  hdmapoc  35547  hlhillcs  35574  fz1eqin  35656  diophin  35660  dvdsabsmod0OLD  35886  divalgmodcl  35887  jm2.19  35893  rmxdiophlem  35915  pw2f1ocnv  35937  wepwsolem  35945  gicabl  36002  sdrgacs  36112  idomodle  36115  isdomn3  36126  extoimad  36652  radcnvrat  36707  bcc0  36733  unima  37467  clim2f  37754  2reu4a  38648  dfdfat2  38671  funbrafv2b  38699  dfafn5a  38700  mod2eq1n2dvds  38763  iccpartgtprec  38772  dfeven2  38817  dfodd3  38818  pfxsuffeqwrdeq  38987  issn  39035  leaddsuble  39085  ausgrusgrb  39300  usgredgffibi  39440  nb3grpr2  39507  cplgr2v  39549  umgr2v2enb1  39613  upgrspths1wlk  39770  dfconngr1  39929  isfusgracl  40011  lindslinindimp2lem4  40527  snlindsntor  40537  regt1loggt0  40620  elbigo2  40636  elbigolo1  40641  fldivexpfllog2  40649  nnlog2ge0lt1  40650  blenpw2m1  40663
  Copyright terms: Public domain W3C validator