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

Theorem bitr4d 259
Description: Deduction form of bitr4i 255. (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 204 . 2  |-  ( ph  ->  ( ch  <->  th )
)
41, 3bitrd 256 1  |-  ( ph  ->  ( ps  <->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187
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 188
This theorem is referenced by:  3bitr2d  284  3bitr2rd  285  3bitr4d  288  3bitr4rd  289  bianabs  888  3anibar  1173  sbcom3  2211  sbal1  2261  sbal2  2262  rmob2  3331  disjprg  4357  reuhypd  4586  opbrop  4871  opelresi  5073  ordsssuc  5466  iota1  5517  funbrfv2b  5864  dffn5  5865  dmfco  5894  fneqeql  5944  f1ompt  5998  dff13  6113  fliftcnv  6158  soisores  6172  isotr  6181  isoini  6183  caovord3  6435  releldm2  6796  brtpos  6932  tpostpos  6943  oe1m  7196  oawordri  7201  oalimcl  7211  omlimcl  7229  omabs  7298  iserd  7339  qliftel  7396  qliftfun  7398  qliftf  7401  ecopovsym  7415  pw2f1olem  7624  mapen  7684  suppeqfsuppbi  7845  funsnfsupp  7855  mapfien  7869  supisolem  7937  cantnflem1  8141  wemapwe  8149  rankr1clem  8238  rankr1c  8239  ranklim  8262  r1pwALT  8264  r1pwcl  8265  isfin1-2  8761  isfin1-4  8763  fin71num  8773  axdc3lem2  8827  ltmnq  9343  prlem936  9418  ltsosr  9464  ltasr  9470  xrlenlt  9645  ltxrlt  9650  letri3  9665  ne0gt0  9685  subadd  9824  ltsubadd2  10031  lesubadd2  10033  suble  10038  ltsub23  10040  ltaddpos2  10051  ltsubpos  10052  subge02  10076  ltord2  10089  leord2  10090  ltaddsublt  10185  divmul  10219  divmul3  10221  rec11r  10252  ltdiv1  10415  ltdivmul2  10428  ledivmul2  10430  ltrec  10434  ltdiv2  10438  negfi  10500  negiso  10533  infmrgelbOLD  10541  infmrlbOLD  10543  nnle1eq1  10583  avgle1  10798  avgle2  10799  avgle  10800  nn0le0eq0  10844  elz2  10900  znnnlt1  10910  zleltp1  10933  uzin  11137  difrp  11283  xrltlen  11391  dfle2  11392  xrletri3  11397  qbtwnre  11438  xltnegi  11455  supxrre  11559  supxrre1  11562  infxrre  11568  infmxrreOLD  11572  ixxun  11597  elioo5  11638  elfz5  11738  elfzm11  11811  uzsplit  11812  predfz  11860  flbi  11996  flbi2  11997  fznnfl  12034  zmodid2  12070  2submod  12096  lt2sq  12293  le2sq  12294  sqlecan  12326  bcval5  12448  shftfib  13074  mulre  13123  cnpart  13242  sqrlem6  13250  sqrmo  13254  elicc4abs  13321  abs2difabs  13336  cau4  13358  limsupgre  13480  limsupgreOLD  13481  clim2  13506  ello12  13518  ello1mpt2  13524  elo12  13529  lo1resb  13566  o1resb  13568  climeq  13569  climmpt2  13575  isercoll  13669  caucvgb  13684  fsumss  13729  fsumabs  13799  isumshft  13835  geomulcvg  13870  fprodss  13940  absefib  14190  dvdsval3  14247  dvdseq  14290  ndvdsadd  14327  bitscmp  14350  smupvallem  14395  dvdssq  14466  lcmdvds  14511  isprm3  14571  isprm5  14589  ncoprmgcdgt1b  14594  coprmdvds  14597  phiprmpw  14662  prmdiv  14671  pc11  14767  pcz  14768  pockthlem  14787  prmreclem2  14799  prmreclem4  14801  prmreclem6  14803  1arith  14809  vdwapun  14862  ramval  14898  ramvalOLD  14899  rami  14910  ramcl  14925  pwsle  15328  ercpbllem  15392  invsym  15605  funcres2c  15744  latnle  16269  grpinvcnv  16660  subgacs  16790  eqger  16805  gexdvds2  17175  pgpfi1  17185  pgpfi  17195  lsmass  17258  lssnle  17262  lsmdisj3b  17278  lsmhash  17293  ablsubadd  17392  gsumval3lem2  17478  subgdmdprd  17605  pgpfac1lem2  17646  dvdsr02  17822  drngid2  17929  issubrg3  17974  lssacs  18128  lspsnel5  18156  psrbaglefi  18534  coe1mul2lem1  18798  prmirred  19003  chrdvds  19036  chrcong  19037  chrnzr  19038  znleval  19062  znleval2  19063  cygznlem3  19077  frlmbas  19255  elfilspd  19298  lindfmm  19322  islindf4  19333  islindf5  19334  mdetunilem9  19582  discld  20042  isneip  20058  neiptopnei  20085  lpdifsn  20096  restopnb  20128  restopn2  20130  restdis  20131  restperf  20137  lmbr2  20212  cncls2  20226  cnprest  20242  cnprest2  20243  iscnrm2  20291  ist0-2  20297  cnt0  20299  ist1-3  20302  ishaus2  20304  cmpfi  20360  dfcon2  20371  1stccnp  20414  1stccn  20415  subislly  20433  hausmapdom  20452  kgencn  20508  tx1cn  20561  tx2cn  20562  txcnmpt  20576  txrest  20583  hauseqlcld  20598  tgqtop  20664  qtopcld  20665  qtopcn  20666  ordthmeolem  20753  trfil2  20839  trfil3  20840  trnei  20844  ufildr  20883  fmfg  20901  rnelfm  20905  fmfnfm  20910  elflim  20923  fbflim  20928  flimrest  20935  isflf  20945  cnflf  20954  cnflf2  20955  fclscf  20977  cnfcf  20994  ptcmplem2  21005  ghmcnp  21066  tsmssubm  21094  iscfilu  21240  xmetgt0  21310  prdsxmetlem  21320  elbl2ps  21341  elbl2  21342  blcomps  21345  blcom  21346  xblpnfps  21347  xblpnf  21348  blpnf  21349  xmeter  21385  setsxms  21431  imasf1obl  21440  stdbdbl  21469  metrest  21476  metcn  21495  txmetcn  21500  metuel2  21517  dscopn  21525  xrtgioo  21761  metdstri  21805  metdstriOLD  21820  cncffvrn  21867  cnmpt2pc  21893  iihalf2  21898  icopnfhmeo  21908  evth2  21925  lmmbr3  22167  iscau3  22185  lmclimf  22210  metcld  22212  cfilucfil3  22225  srabn  22264  rrxmet  22299  minveclem4  22311  minveclem4OLD  22323  evthicc2  22348  ovolfioo  22357  ovolficc  22358  ovolgelb  22370  ovoliun  22395  shft2rab  22398  ovolshftlem1  22399  sca2rab  22402  ovolscalem1  22403  ismbl2  22418  ioombl1lem4  22451  mbfmulc2lem  22540  mbfmax  22542  mbfposr  22545  ismbf3d  22547  mbfaddlem  22553  mbfsup  22557  mbfinf  22558  mbfinfOLD  22559  i1f1lem  22584  i1fmulclem  22597  mbfi1fseqlem4  22613  itg2seq  22637  itg2monolem1  22645  itg2cnlem1  22656  itgfsum  22721  ditgneg  22749  limcdif  22768  limcnlp  22770  cnplimc  22779  rolle  22879  mvth  22881  dvne0  22900  lhop1lem  22902  itgsubst  22938  mdegle0  22963  deg1leb  22981  deg1le0  22997  q1peqb  23042  coemulhi  23145  dgrlt  23157  plydivlem3  23185  vieta1lem2  23201  aannenlem1  23221  ulmres  23280  reefiso  23340  pilem3  23346  pilem3OLD  23347  ellogdm  23521  root1eq1  23632  angpieqvdlem  23691  angpieqvdlem2  23692  quad2  23702  1cubr  23705  quart  23724  rlimcnp  23828  wilthlem2  23931  sgmss  23970  isppw  23978  dvdsflip  24048  dvdsflsumcom  24054  fsumvma  24078  logfac2  24082  chpchtsum  24084  dchrmulcl  24114  dchreq  24123  dchrresb  24124  bclbnd  24145  bposlem1  24149  bposlem5  24153  lgsneg  24184  lgsquadlem1  24219  lgsquadlem2  24220  m1lgs  24227  dchrisumlem3  24266  dchrisum0lem1  24291  trgcgrg  24497  tgellng  24535  lnrot1  24605  islnopp  24718  ismidb  24757  islmib  24766  isleag  24820  ttgelitv  24850  axsegconlem6  24889  axeuclidlem  24929  axcontlem2  24932  axcontlem4  24934  axcontlem12  24942  dfconngra1  25336  clwwlkn2  25440  eupath2  25645  frgra3v  25667  drngoi  26072  nmoreltpnf  26347  isblo2  26361  nmlnogt0  26375  phoeqi  26436  ubthlem2  26450  hire  26684  normgt0  26717  ho01i  27418  ho02i  27419  hoeq1  27420  hoeq2  27421  nmopreltpnf  27459  adjeq  27525  leop  27713  leopmul2i  27725  pjnormssi  27758  pjimai  27766  jplem1  27858  mddmd2  27899  mdslmd1lem1  27915  mdslmd1lem2  27916  superpos  27944  atnssm0  27966  dmdbr5ati  28012  disjunsn  28145  fcoinvbr  28156  feqmptdf  28199  ofpreima  28209  funcnv5mpt  28213  isoun  28223  fpwrelmapffslem  28262  fpwrelmap  28263  xgepnf  28272  xlemnf  28273  xrge0infssdOLD  28288  iocinioc2  28306  xrdifh  28307  nndiffz1  28311  xdivmul  28340  isarchi2  28448  smatrcl  28569  fimaproj  28607  sqsscirc2  28662  xrmulc1cn  28683  ismntoplly  28776  esumfsup  28838  esum2dlem  28860  1stmbfm  29029  2ndmbfm  29030  mbfmcnt  29037  oms0OLD  29076  eulerpartlems  29140  eulerpartlemd  29146  ballotlemfc0  29272  ballotlemfcc  29273  ballotlemsima  29295  ballotlemfrcn0  29309  ballotlemsimaOLD  29333  ballotlemfrcn0OLD  29347  sgn3da  29359  bnj1173  29758  erdszelem7  29867  erdszelem9  29869  iscvm  29929  cvmlift3lem4  29992  sltval2  30489  fscgr  30791  seglelin  30827  btwnoutside  30836  lineunray  30858  cldbnd  30926  isfne4  30940  fneval  30952  filnetlem4  30981  nndivsub  31061  wl-sbhbt  31789  wl-sbcom2d  31798  wl-sbalnae  31799  wl-ax11-lem8  31829  sin2h  31842  cos2h  31843  ptrest  31846  poimirlem3  31850  poimirlem4  31851  poimirlem22  31869  poimirlem27  31874  mblfinlem3  31886  mblfinlem4  31887  ismblfin  31888  itg2addnclem  31900  itg2addnclem2  31901  itg2gt0cn  31904  iblabsnclem  31912  ftc1anclem6  31929  areacirclem2  31940  areacirclem5  31943  areacirc  31944  cover2  31947  mettrifi  31993  prter3  32365  islshpat  32495  lsatnle  32522  ellkr2  32569  lshpkr  32595  lkr0f2  32639  lduallkr3  32640  lkreqN  32648  cvrval2  32752  isat3  32785  glbconN  32854  hlrelat5N  32878  cvrval4N  32891  atlt  32914  1cvrco  32949  pmaple  33238  isline2  33251  isline4N  33254  elpaddn0  33277  elpadd2at2  33284  cdlemkid4  34413  dia0  34532  cdlemm10N  34598  dibglbN  34646  dihmeetlem4preN  34786  dochkrshp3  34868  dvh4dimlem  34923  lcfl5  34976  mapdpglem3  35155  mapdheq  35208  hdmap1eq  35282  hdmapval2lem  35314  hdmapoc  35414  hlhillcs  35441  fz1eqin  35523  diophin  35527  dvdsabsmod0OLD  35754  divalgmodcl  35755  jm2.19  35761  rmxdiophlem  35783  pw2f1ocnv  35805  wepwsolem  35813  gicabl  35870  sdrgacs  35980  idomodle  35983  isdomn3  35994  extoimad  36520  radcnvrat  36576  bcc0  36602  unima  37332  clim2f  37599  2reu4a  38424  dfdfat2  38446  funbrafv2b  38474  dfafn5a  38475  mod2eq1n2dvds  38538  iccpartgtprec  38547  dfeven2  38592  dfodd3  38593  pfxsuffeqwrdeq  38760  issn  38804  leaddsuble  38840  ausgrusgrb  39010  uhgriedg0edg0  39058  usgredgffibi  39126  nb3grpr2  39188  cplgr2v  39227  isfusgracl  39329  lindslinindimp2lem4  39847  snlindsntor  39857  regt1loggt0  39940  elbigo2  39956  elbigolo1  39961  fldivexpfllog2  39969  nnlog2ge0lt1  39970  blenpw2m1  39983
  Copyright terms: Public domain W3C validator