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  1162  sbcom3  2157  sbal1  2208  sbal2  2209  rmob2  3346  disjprg  4363  reuhypd  4589  ordsssuc  4878  opbrop  4993  opelresi  5197  iota1  5474  funbrfv2b  5818  dffn5  5819  dmfco  5848  fneqeql  5897  f1ompt  5955  dff13  6067  fliftcnv  6110  soisores  6124  isotr  6133  isoini  6135  caovord3  6387  releldm2  6749  brtpos  6882  tpostpos  6893  oe1m  7112  oawordri  7117  oalimcl  7127  omlimcl  7145  omabs  7214  iserd  7255  qliftel  7312  qliftfun  7314  qliftf  7317  ecopovsym  7331  pw2f1olem  7540  mapen  7600  suppeqfsuppbi  7758  funsnfsupp  7768  mapfien  7782  supisolem  7846  wemapso2OLD  7892  cantnflem1  8021  cantnflem1OLD  8044  mapfienOLD  8051  wemapwe  8052  wemapweOLD  8053  rankr1clem  8151  rankr1c  8152  ranklim  8175  r1pwALT  8177  r1pwcl  8178  isfin1-2  8678  isfin1-4  8680  fin71num  8690  axdc3lem2  8744  ltmnq  9261  prlem936  9336  ltsosr  9382  ltasr  9388  xrlenlt  9563  ltxrlt  9566  letri3  9581  ne0gt0  9600  subadd  9736  ltsubadd2  9941  lesubadd2  9943  suble  9948  ltsub23  9950  ltaddpos2  9961  ltsubpos  9962  subge02  9986  ltord2  9999  leord2  10000  ltaddsublt  10093  divmul  10127  divmul3  10129  rec11r  10160  ltdiv1  10323  ltdivmul2  10336  ledivmul2  10338  ltrec  10342  ltdiv2  10346  negiso  10435  infmrgelb  10439  infmrlb  10440  nnle1eq1  10480  avgle1  10695  avgle2  10696  avgle  10697  nn0le0eq0  10741  elz2  10798  znnnlt1  10808  zleltp1  10831  uzin  11033  difrp  11173  xrltlen  11273  dfle2  11274  xrletri3  11279  qbtwnre  11319  xltnegi  11336  supxrre  11440  supxrre1  11443  infmxrre  11448  ixxun  11466  elioo5  11503  elfz5  11601  elfzm11  11671  uzsplit  11672  flbi  11851  flbi2  11852  fznnfl  11889  zmodid2  11925  2submod  11951  lt2sq  12144  le2sq  12145  sqlecan  12177  bcval5  12298  shftfib  12907  mulre  12956  cnpart  13075  sqrlem6  13083  sqrmo  13087  elicc4abs  13154  abs2difabs  13169  cau4  13191  limsupgre  13306  clim2  13329  ello12  13341  ello1mpt2  13347  elo12  13352  lo1resb  13389  o1resb  13391  climeq  13392  climmpt2  13398  isercoll  13492  caucvgb  13504  fsumss  13549  fsumabs  13617  isumshft  13653  geomulcvg  13687  fprodss  13757  absefib  13935  dvdsval3  13992  dvdseq  14035  ndvdsadd  14068  bitscmp  14090  smupvallem  14135  dvdssq  14200  isprm3  14228  coprmdvds  14245  isprm5  14255  phiprmpw  14308  prmdiv  14317  pc11  14405  pcz  14406  pockthlem  14425  prmreclem2  14437  prmreclem4  14439  prmreclem6  14441  1arith  14447  vdwapun  14494  ramval  14528  rami  14535  ramcl  14549  pwsle  14899  ercpbllem  14955  invsym  15168  funcres2c  15307  latnle  15832  grpinvcnv  16223  subgacs  16353  eqger  16368  gexdvds2  16722  pgpfi1  16732  pgpfi  16742  lsmass  16805  lssnle  16809  lsmdisj3b  16825  lsmhash  16840  ablsubadd  16939  gsumval3OLD  17025  gsumval3lem2  17027  subgdmdprd  17194  pgpfac1lem2  17239  dvdsr02  17418  drngid2  17525  issubrg3  17570  lssacs  17726  lspsnel5  17754  psrbaglefi  18136  psrbaglefiOLD  18137  coe1mul2lem1  18421  prmirred  18625  chrdvds  18658  chrcong  18659  chrnzr  18660  znleval  18684  znleval2  18685  cygznlem3  18699  frlmbas  18877  elfilspd  18923  lindfmm  18947  islindf4  18958  islindf5  18959  mdetunilem9  19207  discld  19676  isneip  19692  neiptopnei  19719  lpdifsn  19730  restopnb  19762  restopn2  19764  restdis  19765  restperf  19771  lmbr2  19846  cncls2  19860  cnprest  19876  cnprest2  19877  iscnrm2  19925  ist0-2  19931  cnt0  19933  ist1-3  19936  ishaus2  19938  cmpfi  19994  dfcon2  20005  1stccnp  20048  1stccn  20049  subislly  20067  hausmapdom  20086  kgencn  20142  tx1cn  20195  tx2cn  20196  txcnmpt  20210  txrest  20217  hauseqlcld  20232  tgqtop  20298  qtopcld  20299  qtopcn  20300  ordthmeolem  20387  trfil2  20473  trfil3  20474  trnei  20478  ufildr  20517  fmfg  20535  rnelfm  20539  fmfnfm  20544  elflim  20557  fbflim  20562  flimrest  20569  isflf  20579  cnflf  20588  cnflf2  20589  fclscf  20611  cnfcf  20628  ptcmplem2  20638  ghmcnp  20698  tsmssubm  20729  iscfilu  20876  xmetgt0  20946  prdsxmetlem  20956  elbl2ps  20977  elbl2  20978  blcomps  20981  blcom  20982  xblpnfps  20983  xblpnf  20984  blpnf  20985  xmeter  21021  setsxms  21067  imasf1obl  21076  stdbdbl  21105  metrest  21112  metcn  21131  txmetcn  21136  metuel2  21167  dscopn  21179  xrtgioo  21396  metdstri  21440  cncffvrn  21487  cnmpt2pc  21513  iihalf2  21518  icopnfhmeo  21528  evth2  21545  lmmbr3  21784  iscau3  21802  lmclimf  21827  metcld  21829  cfilucfil3OLD  21842  cfilucfil3  21843  srabn  21885  rrxmet  21920  minveclem4  21932  evthicc2  21957  ovolfioo  21964  ovolficc  21965  ovolgelb  21976  ovoliun  22001  shft2rab  22004  ovolshftlem1  22005  sca2rab  22008  ovolscalem1  22009  ismbl2  22023  ioombl1lem4  22056  mbfmulc2lem  22139  mbfmax  22141  mbfposr  22144  ismbf3d  22146  mbfaddlem  22152  mbfsup  22156  mbfinf  22157  i1f1lem  22181  i1fmulclem  22194  mbfi1fseqlem4  22210  itg2seq  22234  itg2monolem1  22242  itg2cnlem1  22253  itgfsum  22318  ditgneg  22346  limcdif  22365  limcnlp  22367  cnplimc  22376  rolle  22476  mvth  22478  dvne0  22497  lhop1lem  22499  itgsubst  22535  mdegle0  22562  deg1leb  22580  deg1le0  22597  q1peqb  22640  coemulhi  22736  dgrlt  22748  plydivlem3  22776  vieta1lem2  22792  aannenlem1  22809  ulmres  22868  reefiso  22928  pilem3  22933  ellogdm  23107  root1eq1  23216  angpieqvdlem  23275  angpieqvdlem2  23276  quad2  23286  1cubr  23289  quart  23308  rlimcnp  23412  wilthlem2  23460  sgmss  23497  isppw  23505  dvdsflip  23575  dvdsflsumcom  23581  fsumvma  23605  logfac2  23609  chpchtsum  23611  dchrmulcl  23641  dchreq  23650  dchrresb  23651  bclbnd  23672  bposlem1  23676  bposlem5  23680  lgsneg  23711  lgsquadlem1  23746  lgsquadlem2  23747  m1lgs  23754  dchrisumlem3  23793  dchrisum0lem1  23818  trgcgrg  24026  tgellng  24060  lnrot1  24123  islnopp  24233  ismidb  24264  islmib  24273  ttgelitv  24307  axsegconlem6  24346  axeuclidlem  24386  axcontlem2  24389  axcontlem4  24391  axcontlem12  24399  dfconngra1  24792  clwwlkn2  24896  eupath2  25101  frgra3v  25123  drngoi  25526  nmoreltpnf  25801  isblo2  25815  nmlnogt0  25829  phoeqi  25890  ubthlem2  25904  hire  26128  normgt0  26161  ho01i  26863  ho02i  26864  hoeq1  26865  hoeq2  26866  nmopreltpnf  26904  adjeq  26970  leop  27158  leopmul2i  27170  pjnormssi  27203  pjimai  27211  jplem1  27303  mddmd2  27344  mdslmd1lem1  27360  mdslmd1lem2  27361  superpos  27389  atnssm0  27411  dmdbr5ati  27457  disjunsn  27583  fcoinvbr  27594  feqmptdf  27642  ofpreima  27653  funcnv5mpt  27657  isoun  27667  fpwrelmapffslem  27705  fpwrelmap  27706  xgepnf  27720  xlemnf  27721  xrge0infssd  27731  iocinioc2  27743  xrdifh  27744  nndiffz1  27749  xdivmul  27774  isarchi2  27882  fimaproj  27990  sqsscirc2  28045  xrmulc1cn  28066  ismntoplly  28156  esumfsup  28218  esum2dlem  28240  1stmbfm  28387  2ndmbfm  28388  mbfmcnt  28395  oms0  28424  eulerpartlems  28482  eulerpartlemd  28488  ballotlemfc0  28614  ballotlemfcc  28615  ballotlemsima  28637  ballotlemfrcn0  28651  sgn3da  28663  erdszelem7  28830  erdszelem9  28832  iscvm  28893  cvmlift3lem4  28956  predfz  29448  sltval2  29581  fscgr  29883  seglelin  29919  btwnoutside  29928  lineunray  29950  nndivsub  30075  wl-sbhbt  30167  wl-sbcom2d  30176  wl-sbalnae  30177  wl-ax11-lem8  30197  sin2h  30210  cos2h  30211  ptrest  30213  mblfinlem3  30218  mblfinlem4  30219  ismblfin  30220  itg2addnclem  30232  itg2addnclem2  30233  itg2gt0cn  30236  iblabsnclem  30244  ftc1anclem6  30261  areacirclem2  30274  areacirclem5  30277  areacirc  30278  cldbnd  30310  isfne4  30324  fneval  30336  filnetlem4  30365  cover2  30370  mettrifi  30416  prter3  30789  fz1eqin  30867  diophin  30871  dvdsabsmod0OLD  31094  divalgmodcl  31095  jm2.19  31101  rmxdiophlem  31123  pw2f1ocnv  31145  wepwsolem  31153  gicabl  31215  sdrgacs  31318  idomodle  31321  isdomn3  31332  radcnvrat  31363  lcmdvds  31382  bcc0  31413  unima  31608  clim2f  31808  2reu4a  32360  dfdfat2  32382  funbrafv2b  32410  dfafn5a  32411  mod2eq1n2dvds  32462  dfeven2  32492  dfodd3  32493  pfxsuffeqwrdeq  32581  leaddsuble  32640  isfusgracl  32744  lindslinindimp2lem4  33262  snlindsntor  33272  regt1loggt0  33357  elbigo2  33373  elbigolo1  33378  fldivexpfllog2  33386  nnlog2ge0lt1  33387  blenpw2m1  33400  bnj1173  34405  islshpat  35155  lsatnle  35182  ellkr2  35229  lshpkr  35255  lkr0f2  35299  lduallkr3  35300  lkreqN  35308  cvrval2  35412  isat3  35445  glbconN  35514  hlrelat5N  35538  cvrval4N  35551  atlt  35574  1cvrco  35609  pmaple  35898  isline2  35911  isline4N  35914  elpaddn0  35937  elpadd2at2  35944  cdlemkid4  37073  dia0  37192  cdlemm10N  37258  dibglbN  37306  dihmeetlem4preN  37446  dochkrshp3  37528  dvh4dimlem  37583  lcfl5  37636  mapdpglem3  37815  mapdheq  37868  hdmap1eq  37942  hdmapval2lem  37974  hdmapoc  38074  hlhillcs  38101  extoimad  38510
  Copyright terms: Public domain W3C validator