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

Theorem bitr4d 247
Description: Deduction form of bitr4i 243. (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 192 . 2  |-  ( ph  ->  ( ch  <->  th )
)
41, 3bitrd 244 1  |-  ( ph  ->  ( ps  <->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  3bitr2d  272  3bitr2rd  273  3bitr4d  276  3bitr4rd  277  bianabs  850  3anibar  1123  disjprg  4019  ordsssuc  4479  reuhypd  4561  opbrop  4767  opelresiOLD  4966  opelresi  4967  iota1  5233  funbrfv2b  5567  dffn5  5568  dmfco  5593  fneqeql  5633  f1ompt  5682  dff13  5783  fliftcnv  5810  soisores  5824  isotr  5833  isoini  5835  caovord3  6033  releldm2  6170  brtpos  6243  tpostpos  6254  riota1  6323  riota2df  6325  riotasvdOLD  6348  oe1m  6543  oawordri  6548  oalimcl  6558  omlimcl  6576  omabs  6645  iserd  6686  qliftel  6741  qliftfun  6743  qliftf  6746  ecopovsym  6760  pw2f1olem  6966  mapen  7025  supisolem  7221  wemapso2  7267  cantnflem1  7391  mapfien  7399  wemapwe  7400  rankr1clem  7492  rankr1c  7493  ranklim  7516  r1pwOLD  7518  r1pwcl  7519  isfin1-2  8011  isfin1-4  8013  fin71num  8023  axdc3lem2  8077  ltmnq  8596  prlem936  8671  ltsosr  8716  ltasr  8722  xrlenlt  8890  ltxrlt  8893  letri3  8907  ne0gt0  8925  subadd  9054  ltsubadd2  9245  lesubadd2  9247  suble  9252  ltsub23  9254  ltaddpos2  9265  ltsubpos  9266  subge02  9289  ltord2  9302  leord2  9303  divmul  9427  divmul3  9429  rec11r  9459  ltdiv1  9620  ltdivmul2  9631  ledivmul2  9633  ltrec  9637  ltdiv2  9641  negiso  9730  infmrgelb  9734  infmrlb  9735  nnle1eq1  9774  avgle1  9951  avgle2  9952  avgle  9953  nn0le0eq0  9994  elz2  10040  znnnlt1  10050  zleltp1  10068  uzin  10260  difrp  10387  xrltlen  10480  dfle2  10481  xrletri3  10486  qbtwnre  10526  xltnegi  10543  supxrre  10646  supxrre1  10649  infmxrre  10654  ixxun  10672  elioo5  10708  elfz5  10790  elfzm11  10853  uzsplit  10855  flbi  10946  flbi2  10947  fznnfl  10966  lt2sq  11177  le2sq  11178  sqlecan  11209  bcval5  11330  shftfib  11567  mulre  11606  cnpart  11725  sqrlem6  11733  sqrmo  11737  elicc4abs  11803  abs2difabs  11818  cau4  11840  limsupgre  11955  clim2  11978  ello12  11990  ello1mpt2  11996  elo12  12001  lo1resb  12038  o1resb  12040  climeq  12041  climmpt2  12047  isercoll  12141  caucvgb  12152  fsumss  12198  fsumabs  12259  isumshft  12298  geomulcvg  12332  absefib  12478  xpnnenOLD  12488  dvdsval3  12535  dvdseq  12576  ndvdsadd  12607  bitscmp  12629  smupvallem  12674  dvdssq  12739  isprm3  12767  coprmdvds  12781  isprm5  12791  phiprmpw  12844  prmdiv  12853  pc11  12932  pcz  12933  pockthlem  12952  prmreclem2  12964  prmreclem4  12966  prmreclem6  12968  1arith  12974  vdwapun  13021  ramval  13055  rami  13062  ramcl  13076  pwsle  13391  ercpbllem  13450  invsym  13664  funcres2c  13775  latnle  14191  ismgmid  14387  grpinvcnv  14536  subgacs  14652  eqger  14667  gexdvds2  14896  pgpfi1  14906  pgpfi  14916  lsmass  14979  lssnle  14983  lsmdisj3b  14999  lsmhash  15014  ablsubadd  15113  gsumval3  15191  subgdmdprd  15269  pgpfac1lem2  15310  dvdsr02  15438  drngid2  15528  issubrg3  15573  lssacs  15724  lspsnel5  15752  psrbaglefi  16118  coe1mul2lem1  16344  prmirred  16448  chrdvds  16482  chrcong  16483  chrnzr  16484  znleval  16508  znleval2  16509  cygznlem3  16523  discld  16826  isneip  16842  lpdifsn  16875  restopnb  16906  restopn2  16908  restdis  16909  restperf  16914  lmbr2  16989  cncls2  17002  cnprest  17017  cnprest2  17018  iscnrm2  17066  ist0-2  17072  cnt0  17074  ist1-3  17077  ishaus2  17079  cmpfi  17135  dfcon2  17145  1stccnp  17188  1stccn  17189  subislly  17207  hausmapdom  17226  kgencn  17251  tx1cn  17303  tx2cn  17304  txcnmpt  17318  txrest  17325  hauseqlcld  17340  tgqtop  17403  qtopcld  17404  qtopcn  17405  ordthmeolem  17492  trfil2  17582  trfil3  17583  trnei  17587  ufildr  17626  fmfg  17644  rnelfm  17648  fmfnfm  17653  elflim  17666  fbflim  17671  flimrest  17678  isflf  17688  cnflf  17697  cnflf2  17698  fclscf  17720  cnfcf  17737  ptcmplem2  17747  ghmcnp  17797  tsmssubm  17825  xmetgt0  17922  prdsxmetlem  17932  elbl2  17950  blcom  17952  xblpnf  17953  blpnf  17954  xmeter  17979  setsxms  18025  imasf1obl  18034  stdbdbl  18063  metrest  18070  metcn  18089  txmetcn  18094  dscopn  18096  xrtgioo  18312  metdstri  18355  cncffvrn  18402  cnmpt2pc  18426  iihalf2  18431  icopnfhmeo  18441  evth2  18458  lmmbr3  18686  iscau3  18704  lmclimf  18729  metcld  18731  srabn  18777  minveclem4  18796  evthicc2  18820  ovolfioo  18827  ovolficc  18828  ovolgelb  18839  ovoliun  18864  shft2rab  18867  ovolshftlem1  18868  sca2rab  18871  ovolscalem1  18872  ismbl2  18886  ioombl1lem4  18918  mbfmulc2lem  19002  mbfmax  19004  mbfposr  19007  ismbf3d  19009  mbfaddlem  19015  mbfsup  19019  mbfinf  19020  i1f1lem  19044  i1fmulclem  19057  mbfi1fseqlem4  19073  itg2seq  19097  itg2monolem1  19105  itg2cnlem1  19116  itgfsum  19181  ditgneg  19207  limcdif  19226  limcnlp  19228  cnplimc  19237  rolle  19337  mvth  19339  dvne0  19358  lhop1lem  19360  itgsubst  19396  mdegle0  19463  deg1leb  19481  deg1le0  19497  q1peqb  19540  coemulhi  19635  dgrlt  19647  plydivlem3  19675  vieta1lem2  19691  aannenlem1  19708  ulmres  19767  reefiso  19824  pilem3  19829  ellogdm  19986  root1eq1  20095  angpieqvdlem  20125  angpieqvdlem2  20126  quad2  20135  1cubr  20138  quart  20157  rlimcnp  20260  wilthlem2  20307  sgmss  20344  isppw  20352  dvdsflip  20422  dvdsflsumcom  20428  fsumvma  20452  fsumvma2  20453  logfac2  20456  chpchtsum  20458  dchrmulcl  20488  dchreq  20497  dchrresb  20498  bclbnd  20519  bposlem1  20523  bposlem5  20527  lgsneg  20558  lgsquadlem1  20593  lgsquadlem2  20594  m1lgs  20601  dchrisumlem3  20640  dchrisum0lem1  20665  drngoi  21074  nmoreltpnf  21347  isblo2  21361  nmlnogt0  21375  phoeqi  21436  ubthlem2  21450  hire  21673  normgt0  21706  ho01i  22408  ho02i  22409  hoeq1  22410  hoeq2  22411  nmopreltpnf  22449  adjeq  22515  leop  22703  leopmul2i  22715  pjnormssi  22748  pjimai  22756  jplem1  22848  mddmd2  22889  mdslmd1lem1  22905  mdslmd1lem2  22906  superpos  22934  atnssm0  22956  dmdbr5ati  23002  ballotlemfc0  23051  ballotlemfcc  23052  ballotlemsima  23074  ballotlemfrcn0  23088  xdivmul  23108  xgtpnf  23114  feqmptdf  23228  funcnv5mpt  23236  isoun  23242  iocinioc2  23272  xrdifh  23273  sqsscirc2  23293  xrmulc1cn  23303  1stmbfm  23565  2ndmbfm  23566  mbfmcnt  23573  erdszelem7  23728  erdszelem9  23730  iscvm  23790  cvmlift3lem4  23853  eupath2  23904  zmodid2  24010  predfz  24203  sltval2  24310  dffun10  24453  axsegconlem6  24550  axeuclidlem  24590  axcontlem2  24593  axcontlem4  24595  axcontlem12  24603  fscgr  24703  seglelin  24739  btwnoutside  24748  lineunray  24770  nndivsub  24896  areacirclem4  24927  areacirclem6  24930  areacirc  24931  iscst4  25177  subaddv  25671  cldbnd  26244  isfne4  26269  fneval  26287  filnetlem4  26330  cover2  26358  mettrifi  26473  prter3  26750  fz1eqin  26848  diophin  26852  dvdsabsmod0  27079  divalgmodcl  27080  jm2.19  27086  rmxdiophlem  27108  pw2f1ocnv  27130  wepwsolem  27138  elfilspd  27255  gicabl  27263  lindfmm  27297  islindf4  27308  islindf5  27309  sdrgacs  27509  idomodle  27512  isdomn3  27523  2reu4a  27967  dfdfat2  27994  funbrafv2b  28021  dfafn5a  28022  frgra3v  28180  sbcoreleleq  28298  bnj1173  29032  islshpat  29207  lsatnle  29234  ellkr2  29281  lshpkr  29307  lkr0f2  29351  lduallkr3  29352  lkreqN  29360  cvrval2  29464  isat3  29497  glbconN  29566  hlrelat5N  29590  cvrval4N  29603  atlt  29626  1cvrco  29661  pmaple  29950  isline2  29963  isline4N  29966  elpaddn0  29989  elpadd2at2  29996  cdlemkid4  31123  dia0  31242  cdlemm10N  31308  dibglbN  31356  dihmeetlem4preN  31496  dochkrshp3  31578  dvh4dimlem  31633  lcfl5  31686  mapdpglem3  31865  mapdheq  31918  hdmap1eq  31992  hdmapval2lem  32024  hdmapoc  32124  hlhillcs  32151
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator