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

Theorem bitr4d 248
Description: Deduction form of bitr4i 244. (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 193 . 2  |-  ( ph  ->  ( ch  <->  th )
)
41, 3bitrd 245 1  |-  ( ph  ->  ( ps  <->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  3bitr2d  273  3bitr2rd  274  3bitr4d  277  3bitr4rd  278  bianabs  851  3anibar  1125  disjprg  4149  ordsssuc  4608  reuhypd  4690  opbrop  4895  opelresiOLD  5097  opelresi  5098  iota1  5372  funbrfv2b  5710  dffn5  5711  dmfco  5736  fneqeql  5777  f1ompt  5830  dff13  5943  fliftcnv  5972  soisores  5986  isotr  5995  isoini  5997  caovord3  6199  releldm2  6336  brtpos  6424  tpostpos  6435  riota1  6504  riota2df  6506  riotasvdOLD  6529  oe1m  6724  oawordri  6729  oalimcl  6739  omlimcl  6757  omabs  6826  iserd  6867  qliftel  6923  qliftfun  6925  qliftf  6928  ecopovsym  6942  pw2f1olem  7148  mapen  7207  supisolem  7408  wemapso2  7454  cantnflem1  7578  mapfien  7586  wemapwe  7587  rankr1clem  7679  rankr1c  7680  ranklim  7703  r1pwOLD  7705  r1pwcl  7706  isfin1-2  8198  isfin1-4  8200  fin71num  8210  axdc3lem2  8264  ltmnq  8782  prlem936  8857  ltsosr  8902  ltasr  8908  xrlenlt  9076  ltxrlt  9079  letri3  9093  ne0gt0  9111  subadd  9240  ltsubadd2  9431  lesubadd2  9433  suble  9438  ltsub23  9440  ltaddpos2  9451  ltsubpos  9452  subge02  9475  ltord2  9488  leord2  9489  divmul  9613  divmul3  9615  rec11r  9645  ltdiv1  9806  ltdivmul2  9817  ledivmul2  9819  ltrec  9823  ltdiv2  9827  negiso  9916  infmrgelb  9920  infmrlb  9921  nnle1eq1  9960  avgle1  10139  avgle2  10140  avgle  10141  nn0le0eq0  10182  elz2  10230  znnnlt1  10240  zleltp1  10258  uzin  10450  difrp  10577  xrltlen  10671  dfle2  10672  xrletri3  10677  qbtwnre  10717  xltnegi  10734  supxrre  10838  supxrre1  10841  infmxrre  10846  ixxun  10864  elioo5  10900  elfz5  10983  elfzm11  11046  uzsplit  11048  flbi  11150  flbi2  11151  fznnfl  11170  lt2sq  11382  le2sq  11383  sqlecan  11414  bcval5  11536  shftfib  11814  mulre  11853  cnpart  11972  sqrlem6  11980  sqrmo  11984  elicc4abs  12050  abs2difabs  12065  cau4  12087  limsupgre  12202  clim2  12225  ello12  12237  ello1mpt2  12243  elo12  12248  lo1resb  12285  o1resb  12287  climeq  12288  climmpt2  12294  isercoll  12388  caucvgb  12400  fsumss  12446  fsumabs  12507  isumshft  12546  geomulcvg  12580  absefib  12726  xpnnenOLD  12736  dvdsval3  12783  dvdseq  12824  ndvdsadd  12855  bitscmp  12877  smupvallem  12922  dvdssq  12987  isprm3  13015  coprmdvds  13029  isprm5  13039  phiprmpw  13092  prmdiv  13101  pc11  13180  pcz  13181  pockthlem  13200  prmreclem2  13212  prmreclem4  13214  prmreclem6  13216  1arith  13222  vdwapun  13269  ramval  13303  rami  13310  ramcl  13324  pwsle  13641  ercpbllem  13700  invsym  13914  funcres2c  14025  latnle  14441  grpinvcnv  14786  subgacs  14902  eqger  14917  gexdvds2  15146  pgpfi1  15156  pgpfi  15166  lsmass  15229  lssnle  15233  lsmdisj3b  15249  lsmhash  15264  ablsubadd  15363  gsumval3  15441  subgdmdprd  15519  pgpfac1lem2  15560  dvdsr02  15688  drngid2  15778  issubrg3  15823  lssacs  15970  lspsnel5  15998  psrbaglefi  16364  coe1mul2lem1  16587  prmirred  16698  chrdvds  16732  chrcong  16733  chrnzr  16734  znleval  16758  znleval2  16759  cygznlem3  16773  discld  17076  isneip  17092  neiptopnei  17119  lpdifsn  17130  restopnb  17161  restopn2  17163  restdis  17164  restperf  17170  lmbr2  17245  cncls2  17259  cnprest  17275  cnprest2  17276  iscnrm2  17324  ist0-2  17330  cnt0  17332  ist1-3  17335  ishaus2  17337  cmpfi  17393  dfcon2  17403  1stccnp  17446  1stccn  17447  subislly  17465  hausmapdom  17484  kgencn  17509  tx1cn  17562  tx2cn  17563  txcnmpt  17577  txrest  17584  hauseqlcld  17599  tgqtop  17665  qtopcld  17666  qtopcn  17667  ordthmeolem  17754  trfil2  17840  trfil3  17841  trnei  17845  ufildr  17884  fmfg  17902  rnelfm  17906  fmfnfm  17911  elflim  17924  fbflim  17929  flimrest  17936  isflf  17946  cnflf  17955  cnflf2  17956  fclscf  17978  cnfcf  17995  ptcmplem2  18005  ghmcnp  18065  tsmssubm  18093  iscfilu  18239  xmetgt0  18296  prdsxmetlem  18306  elbl2  18324  blcom  18326  xblpnf  18327  blpnf  18328  xmeter  18353  setsxms  18399  imasf1obl  18408  stdbdbl  18437  metrest  18444  metcn  18463  txmetcn  18468  metuel2  18485  dscopn  18492  xrtgioo  18708  metdstri  18752  cncffvrn  18799  cnmpt2pc  18824  iihalf2  18829  icopnfhmeo  18839  evth2  18856  lmmbr3  19084  iscau3  19102  lmclimf  19127  metcld  19129  cfilucfil3  19142  srabn  19181  minveclem4  19200  evthicc2  19224  ovolfioo  19231  ovolficc  19232  ovolgelb  19243  ovoliun  19268  shft2rab  19271  ovolshftlem1  19272  sca2rab  19275  ovolscalem1  19276  ismbl2  19290  ioombl1lem4  19322  mbfmulc2lem  19406  mbfmax  19408  mbfposr  19411  ismbf3d  19413  mbfaddlem  19419  mbfsup  19423  mbfinf  19424  i1f1lem  19448  i1fmulclem  19461  mbfi1fseqlem4  19477  itg2seq  19501  itg2monolem1  19509  itg2cnlem1  19520  itgfsum  19585  ditgneg  19611  limcdif  19630  limcnlp  19632  cnplimc  19641  rolle  19741  mvth  19743  dvne0  19762  lhop1lem  19764  itgsubst  19800  mdegle0  19867  deg1leb  19885  deg1le0  19901  q1peqb  19944  coemulhi  20039  dgrlt  20051  plydivlem3  20079  vieta1lem2  20095  aannenlem1  20112  ulmres  20171  reefiso  20231  pilem3  20236  ellogdm  20397  root1eq1  20506  angpieqvdlem  20536  angpieqvdlem2  20537  quad2  20546  1cubr  20549  quart  20568  rlimcnp  20671  wilthlem2  20719  sgmss  20756  isppw  20764  dvdsflip  20834  dvdsflsumcom  20840  fsumvma  20864  logfac2  20868  chpchtsum  20870  dchrmulcl  20900  dchreq  20909  dchrresb  20910  bclbnd  20931  bposlem1  20935  bposlem5  20939  lgsneg  20970  lgsquadlem1  21005  lgsquadlem2  21006  m1lgs  21013  dchrisumlem3  21052  dchrisum0lem1  21077  dfconngra1  21506  eupath2  21550  drngoi  21843  nmoreltpnf  22118  isblo2  22132  nmlnogt0  22146  phoeqi  22207  ubthlem2  22221  hire  22444  normgt0  22477  ho01i  23179  ho02i  23180  hoeq1  23181  hoeq2  23182  nmopreltpnf  23220  adjeq  23286  leop  23474  leopmul2i  23486  pjnormssi  23519  pjimai  23527  jplem1  23619  mddmd2  23660  mdslmd1lem1  23676  mdslmd1lem2  23677  superpos  23705  atnssm0  23727  dmdbr5ati  23773  feqmptdf  23917  funcnv5mpt  23925  isoun  23930  iocinioc2  23978  xrdifh  23979  xdivmul  24009  xgtpnf  24015  sqsscirc2  24111  xrmulc1cn  24120  esumfsup  24256  1stmbfm  24404  2ndmbfm  24405  mbfmcnt  24412  ballotlemfc0  24529  ballotlemfcc  24530  ballotlemsima  24552  ballotlemfrcn0  24566  erdszelem7  24662  erdszelem9  24664  iscvm  24725  cvmlift3lem4  24788  zmodid2  24893  fprodss  25053  predfz  25227  sltval2  25334  dffun10  25477  axsegconlem6  25575  axeuclidlem  25615  axcontlem2  25618  axcontlem4  25620  axcontlem12  25628  fscgr  25728  seglelin  25764  btwnoutside  25773  lineunray  25795  nndivsub  25921  itg2addnclem  25957  itg2addnclem2  25958  itg2gt0cn  25960  itgaddnclem2  25964  iblabsnclem  25968  areacirclem4  25984  areacirclem6  25987  areacirc  25988  cldbnd  26020  isfne4  26040  fneval  26058  filnetlem4  26101  cover2  26106  mettrifi  26154  prter3  26422  fz1eqin  26518  diophin  26522  dvdsabsmod0  26748  divalgmodcl  26749  jm2.19  26755  rmxdiophlem  26777  pw2f1ocnv  26799  wepwsolem  26807  elfilspd  26924  gicabl  26932  lindfmm  26966  islindf4  26977  islindf5  26978  sdrgacs  27178  idomodle  27181  isdomn3  27192  2reu4a  27635  dfdfat2  27664  funbrafv2b  27692  dfafn5a  27693  frgra3v  27755  sbcoreleleq  27962  bnj1173  28709  islshpat  29132  lsatnle  29159  ellkr2  29206  lshpkr  29232  lkr0f2  29276  lduallkr3  29277  lkreqN  29285  cvrval2  29389  isat3  29422  glbconN  29491  hlrelat5N  29515  cvrval4N  29528  atlt  29551  1cvrco  29586  pmaple  29875  isline2  29888  isline4N  29891  elpaddn0  29914  elpadd2at2  29921  cdlemkid4  31048  dia0  31167  cdlemm10N  31233  dibglbN  31281  dihmeetlem4preN  31421  dochkrshp3  31503  dvh4dimlem  31558  lcfl5  31611  mapdpglem3  31790  mapdheq  31843  hdmap1eq  31917  hdmapval2lem  31949  hdmapoc  32049  hlhillcs  32076
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 178
  Copyright terms: Public domain W3C validator