MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bitr4d Structured version   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  4200  ordsssuc  4660  reuhypd  4742  opbrop  4947  opelresiOLD  5149  opelresi  5150  iota1  5424  funbrfv2b  5763  dffn5  5764  dmfco  5789  fneqeql  5830  f1ompt  5883  dff13  5996  fliftcnv  6025  soisores  6039  isotr  6048  isoini  6050  caovord3  6252  releldm2  6389  brtpos  6480  tpostpos  6491  riota1  6560  riota2df  6562  riotasvdOLD  6585  oe1m  6780  oawordri  6785  oalimcl  6795  omlimcl  6813  omabs  6882  iserd  6923  qliftel  6979  qliftfun  6981  qliftf  6984  ecopovsym  6998  pw2f1olem  7204  mapen  7263  supisolem  7467  wemapso2  7513  cantnflem1  7637  mapfien  7645  wemapwe  7646  rankr1clem  7738  rankr1c  7739  ranklim  7762  r1pwOLD  7764  r1pwcl  7765  isfin1-2  8257  isfin1-4  8259  fin71num  8269  axdc3lem2  8323  ltmnq  8841  prlem936  8916  ltsosr  8961  ltasr  8967  xrlenlt  9135  ltxrlt  9138  letri3  9152  ne0gt0  9170  subadd  9300  ltsubadd2  9491  lesubadd2  9493  suble  9498  ltsub23  9500  ltaddpos2  9511  ltsubpos  9512  subge02  9535  ltord2  9548  leord2  9549  divmul  9673  divmul3  9675  rec11r  9705  ltdiv1  9866  ltdivmul2  9877  ledivmul2  9879  ltrec  9883  ltdiv2  9887  negiso  9976  infmrgelb  9980  infmrlb  9981  nnle1eq1  10020  avgle1  10199  avgle2  10200  avgle  10201  nn0le0eq0  10242  elz2  10290  znnnlt1  10300  zleltp1  10318  uzin  10510  difrp  10637  xrltlen  10731  dfle2  10732  xrletri3  10737  qbtwnre  10777  xltnegi  10794  supxrre  10898  supxrre1  10901  infmxrre  10906  ixxun  10924  elioo5  10960  elfz5  11043  elfzm11  11108  uzsplit  11110  flbi  11215  flbi2  11216  fznnfl  11235  lt2sq  11447  le2sq  11448  sqlecan  11479  bcval5  11601  shftfib  11879  mulre  11918  cnpart  12037  sqrlem6  12045  sqrmo  12049  elicc4abs  12115  abs2difabs  12130  cau4  12152  limsupgre  12267  clim2  12290  ello12  12302  ello1mpt2  12308  elo12  12313  lo1resb  12350  o1resb  12352  climeq  12353  climmpt2  12359  isercoll  12453  caucvgb  12465  fsumss  12511  fsumabs  12572  isumshft  12611  geomulcvg  12645  absefib  12791  xpnnenOLD  12801  dvdsval3  12848  dvdseq  12889  ndvdsadd  12920  bitscmp  12942  smupvallem  12987  dvdssq  13052  isprm3  13080  coprmdvds  13094  isprm5  13104  phiprmpw  13157  prmdiv  13166  pc11  13245  pcz  13246  pockthlem  13265  prmreclem2  13277  prmreclem4  13279  prmreclem6  13281  1arith  13287  vdwapun  13334  ramval  13368  rami  13375  ramcl  13389  pwsle  13706  ercpbllem  13765  invsym  13979  funcres2c  14090  latnle  14506  grpinvcnv  14851  subgacs  14967  eqger  14982  gexdvds2  15211  pgpfi1  15221  pgpfi  15231  lsmass  15294  lssnle  15298  lsmdisj3b  15314  lsmhash  15329  ablsubadd  15428  gsumval3  15506  subgdmdprd  15584  pgpfac1lem2  15625  dvdsr02  15753  drngid2  15843  issubrg3  15888  lssacs  16035  lspsnel5  16063  psrbaglefi  16429  coe1mul2lem1  16652  prmirred  16767  chrdvds  16801  chrcong  16802  chrnzr  16803  znleval  16827  znleval2  16828  cygznlem3  16842  discld  17145  isneip  17161  neiptopnei  17188  lpdifsn  17199  restopnb  17231  restopn2  17233  restdis  17234  restperf  17240  lmbr2  17315  cncls2  17329  cnprest  17345  cnprest2  17346  iscnrm2  17394  ist0-2  17400  cnt0  17402  ist1-3  17405  ishaus2  17407  cmpfi  17463  dfcon2  17474  1stccnp  17517  1stccn  17518  subislly  17536  hausmapdom  17555  kgencn  17580  tx1cn  17633  tx2cn  17634  txcnmpt  17648  txrest  17655  hauseqlcld  17670  tgqtop  17736  qtopcld  17737  qtopcn  17738  ordthmeolem  17825  trfil2  17911  trfil3  17912  trnei  17916  ufildr  17955  fmfg  17973  rnelfm  17977  fmfnfm  17982  elflim  17995  fbflim  18000  flimrest  18007  isflf  18017  cnflf  18026  cnflf2  18027  fclscf  18049  cnfcf  18066  ptcmplem2  18076  ghmcnp  18136  tsmssubm  18164  iscfilu  18310  xmetgt0  18380  prdsxmetlem  18390  elbl2ps  18411  elbl2  18412  blcomps  18415  blcom  18416  xblpnfps  18417  xblpnf  18418  blpnf  18419  xmeter  18455  setsxms  18501  imasf1obl  18510  stdbdbl  18539  metrest  18546  metcn  18565  txmetcn  18570  metuel2  18601  dscopn  18613  xrtgioo  18829  metdstri  18873  cncffvrn  18920  cnmpt2pc  18945  iihalf2  18950  icopnfhmeo  18960  evth2  18977  lmmbr3  19205  iscau3  19223  lmclimf  19248  metcld  19250  cfilucfil3OLD  19263  cfilucfil3  19264  srabn  19306  minveclem4  19325  evthicc2  19349  ovolfioo  19356  ovolficc  19357  ovolgelb  19368  ovoliun  19393  shft2rab  19396  ovolshftlem1  19397  sca2rab  19400  ovolscalem1  19401  ismbl2  19415  ioombl1lem4  19447  mbfmulc2lem  19531  mbfmax  19533  mbfposr  19536  ismbf3d  19538  mbfaddlem  19544  mbfsup  19548  mbfinf  19549  i1f1lem  19573  i1fmulclem  19586  mbfi1fseqlem4  19602  itg2seq  19626  itg2monolem1  19634  itg2cnlem1  19645  itgfsum  19710  ditgneg  19736  limcdif  19755  limcnlp  19757  cnplimc  19766  rolle  19866  mvth  19868  dvne0  19887  lhop1lem  19889  itgsubst  19925  mdegle0  19992  deg1leb  20010  deg1le0  20026  q1peqb  20069  coemulhi  20164  dgrlt  20176  plydivlem3  20204  vieta1lem2  20220  aannenlem1  20237  ulmres  20296  reefiso  20356  pilem3  20361  ellogdm  20522  root1eq1  20631  angpieqvdlem  20661  angpieqvdlem2  20662  quad2  20671  1cubr  20674  quart  20693  rlimcnp  20796  wilthlem2  20844  sgmss  20881  isppw  20889  dvdsflip  20959  dvdsflsumcom  20965  fsumvma  20989  logfac2  20993  chpchtsum  20995  dchrmulcl  21025  dchreq  21034  dchrresb  21035  bclbnd  21056  bposlem1  21060  bposlem5  21064  lgsneg  21095  lgsquadlem1  21130  lgsquadlem2  21131  m1lgs  21138  dchrisumlem3  21177  dchrisum0lem1  21202  dfconngra1  21650  eupath2  21694  drngoi  21987  nmoreltpnf  22262  isblo2  22276  nmlnogt0  22290  phoeqi  22351  ubthlem2  22365  hire  22588  normgt0  22621  ho01i  23323  ho02i  23324  hoeq1  23325  hoeq2  23326  nmopreltpnf  23364  adjeq  23430  leop  23618  leopmul2i  23630  pjnormssi  23663  pjimai  23671  jplem1  23763  mddmd2  23804  mdslmd1lem1  23820  mdslmd1lem2  23821  superpos  23849  atnssm0  23871  dmdbr5ati  23917  feqmptdf  24067  ofpreima  24073  funcnv5mpt  24076  isoun  24081  xgepnf  24108  xlemnf  24109  iocinioc2  24134  xrdifh  24135  xdivmul  24163  isinftm  24243  isarchi2  24247  metidv  24279  pstmxmet  24284  sqsscirc2  24299  xrmulc1cn  24308  esumfsup  24452  1stmbfm  24602  2ndmbfm  24603  mbfmcnt  24610  ballotlemfc0  24742  ballotlemfcc  24743  ballotlemsima  24765  ballotlemfrcn0  24779  erdszelem7  24875  erdszelem9  24877  iscvm  24938  cvmlift3lem4  25001  zmodid2  25106  fprodss  25266  predfz  25470  sltval2  25603  axsegconlem6  25853  axeuclidlem  25893  axcontlem2  25896  axcontlem4  25898  axcontlem12  25906  fscgr  26006  seglelin  26042  btwnoutside  26051  lineunray  26073  nndivsub  26199  mblfinlem2  26235  mblfinlem3  26236  ismblfin  26237  itg2addnclem  26246  itg2addnclem2  26247  itg2gt0cn  26250  iblabsnclem  26258  ftc1anclem6  26275  areacirclem4  26284  areacirclem6  26287  areacirc  26288  cldbnd  26320  isfne4  26340  fneval  26358  filnetlem4  26401  cover2  26406  mettrifi  26454  prter3  26722  fz1eqin  26818  diophin  26822  dvdsabsmod0  27048  divalgmodcl  27049  jm2.19  27055  rmxdiophlem  27077  pw2f1ocnv  27099  wepwsolem  27107  elfilspd  27223  gicabl  27231  lindfmm  27265  islindf4  27276  islindf5  27277  sdrgacs  27477  idomodle  27480  isdomn3  27491  2reu4a  27934  dfdfat2  27962  funbrafv2b  27990  dfafn5a  27991  leaddsuble  28076  2submod  28130  frgra3v  28329  sbcoreleleq  28556  bnj1173  29308  islshpat  29752  lsatnle  29779  ellkr2  29826  lshpkr  29852  lkr0f2  29896  lduallkr3  29897  lkreqN  29905  cvrval2  30009  isat3  30042  glbconN  30111  hlrelat5N  30135  cvrval4N  30148  atlt  30171  1cvrco  30206  pmaple  30495  isline2  30508  isline4N  30511  elpaddn0  30534  elpadd2at2  30541  cdlemkid4  31668  dia0  31787  cdlemm10N  31853  dibglbN  31901  dihmeetlem4preN  32041  dochkrshp3  32123  dvh4dimlem  32178  lcfl5  32231  mapdpglem3  32410  mapdheq  32463  hdmap1eq  32537  hdmapval2lem  32569  hdmapoc  32669  hlhillcs  32696
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