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  4168  ordsssuc  4627  reuhypd  4709  opbrop  4914  opelresiOLD  5116  opelresi  5117  iota1  5391  funbrfv2b  5730  dffn5  5731  dmfco  5756  fneqeql  5797  f1ompt  5850  dff13  5963  fliftcnv  5992  soisores  6006  isotr  6015  isoini  6017  caovord3  6219  releldm2  6356  brtpos  6447  tpostpos  6458  riota1  6527  riota2df  6529  riotasvdOLD  6552  oe1m  6747  oawordri  6752  oalimcl  6762  omlimcl  6780  omabs  6849  iserd  6890  qliftel  6946  qliftfun  6948  qliftf  6951  ecopovsym  6965  pw2f1olem  7171  mapen  7230  supisolem  7431  wemapso2  7477  cantnflem1  7601  mapfien  7609  wemapwe  7610  rankr1clem  7702  rankr1c  7703  ranklim  7726  r1pwOLD  7728  r1pwcl  7729  isfin1-2  8221  isfin1-4  8223  fin71num  8233  axdc3lem2  8287  ltmnq  8805  prlem936  8880  ltsosr  8925  ltasr  8931  xrlenlt  9099  ltxrlt  9102  letri3  9116  ne0gt0  9134  subadd  9264  ltsubadd2  9455  lesubadd2  9457  suble  9462  ltsub23  9464  ltaddpos2  9475  ltsubpos  9476  subge02  9499  ltord2  9512  leord2  9513  divmul  9637  divmul3  9639  rec11r  9669  ltdiv1  9830  ltdivmul2  9841  ledivmul2  9843  ltrec  9847  ltdiv2  9851  negiso  9940  infmrgelb  9944  infmrlb  9945  nnle1eq1  9984  avgle1  10163  avgle2  10164  avgle  10165  nn0le0eq0  10206  elz2  10254  znnnlt1  10264  zleltp1  10282  uzin  10474  difrp  10601  xrltlen  10695  dfle2  10696  xrletri3  10701  qbtwnre  10741  xltnegi  10758  supxrre  10862  supxrre1  10865  infmxrre  10870  ixxun  10888  elioo5  10924  elfz5  11007  elfzm11  11071  uzsplit  11073  flbi  11178  flbi2  11179  fznnfl  11198  lt2sq  11410  le2sq  11411  sqlecan  11442  bcval5  11564  shftfib  11842  mulre  11881  cnpart  12000  sqrlem6  12008  sqrmo  12012  elicc4abs  12078  abs2difabs  12093  cau4  12115  limsupgre  12230  clim2  12253  ello12  12265  ello1mpt2  12271  elo12  12276  lo1resb  12313  o1resb  12315  climeq  12316  climmpt2  12322  isercoll  12416  caucvgb  12428  fsumss  12474  fsumabs  12535  isumshft  12574  geomulcvg  12608  absefib  12754  xpnnenOLD  12764  dvdsval3  12811  dvdseq  12852  ndvdsadd  12883  bitscmp  12905  smupvallem  12950  dvdssq  13015  isprm3  13043  coprmdvds  13057  isprm5  13067  phiprmpw  13120  prmdiv  13129  pc11  13208  pcz  13209  pockthlem  13228  prmreclem2  13240  prmreclem4  13242  prmreclem6  13244  1arith  13250  vdwapun  13297  ramval  13331  rami  13338  ramcl  13352  pwsle  13669  ercpbllem  13728  invsym  13942  funcres2c  14053  latnle  14469  grpinvcnv  14814  subgacs  14930  eqger  14945  gexdvds2  15174  pgpfi1  15184  pgpfi  15194  lsmass  15257  lssnle  15261  lsmdisj3b  15277  lsmhash  15292  ablsubadd  15391  gsumval3  15469  subgdmdprd  15547  pgpfac1lem2  15588  dvdsr02  15716  drngid2  15806  issubrg3  15851  lssacs  15998  lspsnel5  16026  psrbaglefi  16392  coe1mul2lem1  16615  prmirred  16730  chrdvds  16764  chrcong  16765  chrnzr  16766  znleval  16790  znleval2  16791  cygznlem3  16805  discld  17108  isneip  17124  neiptopnei  17151  lpdifsn  17162  restopnb  17193  restopn2  17195  restdis  17196  restperf  17202  lmbr2  17277  cncls2  17291  cnprest  17307  cnprest2  17308  iscnrm2  17356  ist0-2  17362  cnt0  17364  ist1-3  17367  ishaus2  17369  cmpfi  17425  dfcon2  17435  1stccnp  17478  1stccn  17479  subislly  17497  hausmapdom  17516  kgencn  17541  tx1cn  17594  tx2cn  17595  txcnmpt  17609  txrest  17616  hauseqlcld  17631  tgqtop  17697  qtopcld  17698  qtopcn  17699  ordthmeolem  17786  trfil2  17872  trfil3  17873  trnei  17877  ufildr  17916  fmfg  17934  rnelfm  17938  fmfnfm  17943  elflim  17956  fbflim  17961  flimrest  17968  isflf  17978  cnflf  17987  cnflf2  17988  fclscf  18010  cnfcf  18027  ptcmplem2  18037  ghmcnp  18097  tsmssubm  18125  iscfilu  18271  xmetgt0  18341  prdsxmetlem  18351  elbl2ps  18372  elbl2  18373  blcomps  18376  blcom  18377  xblpnfps  18378  xblpnf  18379  blpnf  18380  xmeter  18416  setsxms  18462  imasf1obl  18471  stdbdbl  18500  metrest  18507  metcn  18526  txmetcn  18531  metuel2  18562  dscopn  18574  xrtgioo  18790  metdstri  18834  cncffvrn  18881  cnmpt2pc  18906  iihalf2  18911  icopnfhmeo  18921  evth2  18938  lmmbr3  19166  iscau3  19184  lmclimf  19209  metcld  19211  cfilucfil3OLD  19224  cfilucfil3  19225  srabn  19267  minveclem4  19286  evthicc2  19310  ovolfioo  19317  ovolficc  19318  ovolgelb  19329  ovoliun  19354  shft2rab  19357  ovolshftlem1  19358  sca2rab  19361  ovolscalem1  19362  ismbl2  19376  ioombl1lem4  19408  mbfmulc2lem  19492  mbfmax  19494  mbfposr  19497  ismbf3d  19499  mbfaddlem  19505  mbfsup  19509  mbfinf  19510  i1f1lem  19534  i1fmulclem  19547  mbfi1fseqlem4  19563  itg2seq  19587  itg2monolem1  19595  itg2cnlem1  19606  itgfsum  19671  ditgneg  19697  limcdif  19716  limcnlp  19718  cnplimc  19727  rolle  19827  mvth  19829  dvne0  19848  lhop1lem  19850  itgsubst  19886  mdegle0  19953  deg1leb  19971  deg1le0  19987  q1peqb  20030  coemulhi  20125  dgrlt  20137  plydivlem3  20165  vieta1lem2  20181  aannenlem1  20198  ulmres  20257  reefiso  20317  pilem3  20322  ellogdm  20483  root1eq1  20592  angpieqvdlem  20622  angpieqvdlem2  20623  quad2  20632  1cubr  20635  quart  20654  rlimcnp  20757  wilthlem2  20805  sgmss  20842  isppw  20850  dvdsflip  20920  dvdsflsumcom  20926  fsumvma  20950  logfac2  20954  chpchtsum  20956  dchrmulcl  20986  dchreq  20995  dchrresb  20996  bclbnd  21017  bposlem1  21021  bposlem5  21025  lgsneg  21056  lgsquadlem1  21091  lgsquadlem2  21092  m1lgs  21099  dchrisumlem3  21138  dchrisum0lem1  21163  dfconngra1  21611  eupath2  21655  drngoi  21948  nmoreltpnf  22223  isblo2  22237  nmlnogt0  22251  phoeqi  22312  ubthlem2  22326  hire  22549  normgt0  22582  ho01i  23284  ho02i  23285  hoeq1  23286  hoeq2  23287  nmopreltpnf  23325  adjeq  23391  leop  23579  leopmul2i  23591  pjnormssi  23624  pjimai  23632  jplem1  23724  mddmd2  23765  mdslmd1lem1  23781  mdslmd1lem2  23782  superpos  23810  atnssm0  23832  dmdbr5ati  23878  feqmptdf  24028  ofpreima  24034  funcnv5mpt  24037  isoun  24042  xgepnf  24069  xlemnf  24070  iocinioc2  24095  xrdifh  24096  xdivmul  24124  isinftm  24204  isarchi2  24208  metidv  24240  pstmxmet  24245  sqsscirc2  24260  xrmulc1cn  24269  esumfsup  24413  1stmbfm  24563  2ndmbfm  24564  mbfmcnt  24571  ballotlemfc0  24703  ballotlemfcc  24704  ballotlemsima  24726  ballotlemfrcn0  24740  erdszelem7  24836  erdszelem9  24838  iscvm  24899  cvmlift3lem4  24962  zmodid2  25067  fprodss  25227  predfz  25417  sltval2  25524  dffun10  25667  axsegconlem6  25765  axeuclidlem  25805  axcontlem2  25808  axcontlem4  25810  axcontlem12  25818  fscgr  25918  seglelin  25954  btwnoutside  25963  lineunray  25985  nndivsub  26111  mblfinlem2  26144  mblfinlem3  26145  ismblfin  26146  itg2addnclem  26155  itg2addnclem2  26156  itg2gt0cn  26159  iblabsnclem  26167  areacirclem4  26183  areacirclem6  26186  areacirc  26187  cldbnd  26219  isfne4  26239  fneval  26257  filnetlem4  26300  cover2  26305  mettrifi  26353  prter3  26621  fz1eqin  26717  diophin  26721  dvdsabsmod0  26947  divalgmodcl  26948  jm2.19  26954  rmxdiophlem  26976  pw2f1ocnv  26998  wepwsolem  27006  elfilspd  27123  gicabl  27131  lindfmm  27165  islindf4  27176  islindf5  27177  sdrgacs  27377  idomodle  27380  isdomn3  27391  2reu4a  27834  dfdfat2  27862  funbrafv2b  27890  dfafn5a  27891  leaddsuble  27970  frgra3v  28106  sbcoreleleq  28330  bnj1173  29077  islshpat  29500  lsatnle  29527  ellkr2  29574  lshpkr  29600  lkr0f2  29644  lduallkr3  29645  lkreqN  29653  cvrval2  29757  isat3  29790  glbconN  29859  hlrelat5N  29883  cvrval4N  29896  atlt  29919  1cvrco  29954  pmaple  30243  isline2  30256  isline4N  30259  elpaddn0  30282  elpadd2at2  30289  cdlemkid4  31416  dia0  31535  cdlemm10N  31601  dibglbN  31649  dihmeetlem4preN  31789  dochkrshp3  31871  dvh4dimlem  31926  lcfl5  31979  mapdpglem3  32158  mapdheq  32211  hdmap1eq  32285  hdmapval2lem  32317  hdmapoc  32417  hlhillcs  32444
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