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

Theorem bitr4d 249
Description: Deduction form of bitr4i 245. (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 194 . 2  |-  ( ph  ->  ( ch  <->  th )
)
41, 3bitrd 246 1  |-  ( ph  ->  ( ps  <->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178
This theorem is referenced by:  3bitr2d  274  3bitr2rd  275  3bitr4d  278  3bitr4rd  279  bianabs  852  3anibar  1126  sbcom  2166  disjprg  4210  ordsssuc  4670  reuhypd  4752  opbrop  4957  opelresiOLD  5159  opelresi  5160  iota1  5434  funbrfv2b  5773  dffn5  5774  dmfco  5799  fneqeql  5840  f1ompt  5893  dff13  6006  fliftcnv  6035  soisores  6049  isotr  6058  isoini  6060  caovord3  6262  releldm2  6399  brtpos  6490  tpostpos  6501  riota1  6570  riota2df  6572  riotasvdOLD  6595  oe1m  6790  oawordri  6795  oalimcl  6805  omlimcl  6823  omabs  6892  iserd  6933  qliftel  6989  qliftfun  6991  qliftf  6994  ecopovsym  7008  pw2f1olem  7214  mapen  7273  supisolem  7477  wemapso2  7523  cantnflem1  7647  mapfien  7655  wemapwe  7656  rankr1clem  7748  rankr1c  7749  ranklim  7772  r1pwOLD  7774  r1pwcl  7775  isfin1-2  8267  isfin1-4  8269  fin71num  8279  axdc3lem2  8333  ltmnq  8851  prlem936  8926  ltsosr  8971  ltasr  8977  xrlenlt  9145  ltxrlt  9148  letri3  9162  ne0gt0  9180  subadd  9310  ltsubadd2  9501  lesubadd2  9503  suble  9508  ltsub23  9510  ltaddpos2  9521  ltsubpos  9522  subge02  9545  ltord2  9558  leord2  9559  divmul  9683  divmul3  9685  rec11r  9715  ltdiv1  9876  ltdivmul2  9887  ledivmul2  9889  ltrec  9893  ltdiv2  9897  negiso  9986  infmrgelb  9990  infmrlb  9991  nnle1eq1  10030  avgle1  10209  avgle2  10210  avgle  10211  nn0le0eq0  10252  elz2  10300  znnnlt1  10310  zleltp1  10328  uzin  10520  difrp  10647  xrltlen  10741  dfle2  10742  xrletri3  10747  qbtwnre  10787  xltnegi  10804  supxrre  10908  supxrre1  10911  infmxrre  10916  ixxun  10934  elioo5  10970  elfz5  11053  elfzm11  11118  uzsplit  11120  flbi  11225  flbi2  11226  fznnfl  11245  lt2sq  11457  le2sq  11458  sqlecan  11489  bcval5  11611  shftfib  11889  mulre  11928  cnpart  12047  sqrlem6  12055  sqrmo  12059  elicc4abs  12125  abs2difabs  12140  cau4  12162  limsupgre  12277  clim2  12300  ello12  12312  ello1mpt2  12318  elo12  12323  lo1resb  12360  o1resb  12362  climeq  12363  climmpt2  12369  isercoll  12463  caucvgb  12475  fsumss  12521  fsumabs  12582  isumshft  12621  geomulcvg  12655  absefib  12801  xpnnenOLD  12811  dvdsval3  12858  dvdseq  12899  ndvdsadd  12930  bitscmp  12952  smupvallem  12997  dvdssq  13062  isprm3  13090  coprmdvds  13104  isprm5  13114  phiprmpw  13167  prmdiv  13176  pc11  13255  pcz  13256  pockthlem  13275  prmreclem2  13287  prmreclem4  13289  prmreclem6  13291  1arith  13297  vdwapun  13344  ramval  13378  rami  13385  ramcl  13399  pwsle  13716  ercpbllem  13775  invsym  13989  funcres2c  14100  latnle  14516  grpinvcnv  14861  subgacs  14977  eqger  14992  gexdvds2  15221  pgpfi1  15231  pgpfi  15241  lsmass  15304  lssnle  15308  lsmdisj3b  15324  lsmhash  15339  ablsubadd  15438  gsumval3  15516  subgdmdprd  15594  pgpfac1lem2  15635  dvdsr02  15763  drngid2  15853  issubrg3  15898  lssacs  16045  lspsnel5  16073  psrbaglefi  16439  coe1mul2lem1  16662  prmirred  16777  chrdvds  16811  chrcong  16812  chrnzr  16813  znleval  16837  znleval2  16838  cygznlem3  16852  discld  17155  isneip  17171  neiptopnei  17198  lpdifsn  17209  restopnb  17241  restopn2  17243  restdis  17244  restperf  17250  lmbr2  17325  cncls2  17339  cnprest  17355  cnprest2  17356  iscnrm2  17404  ist0-2  17410  cnt0  17412  ist1-3  17415  ishaus2  17417  cmpfi  17473  dfcon2  17484  1stccnp  17527  1stccn  17528  subislly  17546  hausmapdom  17565  kgencn  17590  tx1cn  17643  tx2cn  17644  txcnmpt  17658  txrest  17665  hauseqlcld  17680  tgqtop  17746  qtopcld  17747  qtopcn  17748  ordthmeolem  17835  trfil2  17921  trfil3  17922  trnei  17926  ufildr  17965  fmfg  17983  rnelfm  17987  fmfnfm  17992  elflim  18005  fbflim  18010  flimrest  18017  isflf  18027  cnflf  18036  cnflf2  18037  fclscf  18059  cnfcf  18076  ptcmplem2  18086  ghmcnp  18146  tsmssubm  18174  iscfilu  18320  xmetgt0  18390  prdsxmetlem  18400  elbl2ps  18421  elbl2  18422  blcomps  18425  blcom  18426  xblpnfps  18427  xblpnf  18428  blpnf  18429  xmeter  18465  setsxms  18511  imasf1obl  18520  stdbdbl  18549  metrest  18556  metcn  18575  txmetcn  18580  metuel2  18611  dscopn  18623  xrtgioo  18839  metdstri  18883  cncffvrn  18930  cnmpt2pc  18955  iihalf2  18960  icopnfhmeo  18970  evth2  18987  lmmbr3  19215  iscau3  19233  lmclimf  19258  metcld  19260  cfilucfil3OLD  19273  cfilucfil3  19274  srabn  19316  minveclem4  19335  evthicc2  19359  ovolfioo  19366  ovolficc  19367  ovolgelb  19378  ovoliun  19403  shft2rab  19406  ovolshftlem1  19407  sca2rab  19410  ovolscalem1  19411  ismbl2  19425  ioombl1lem4  19457  mbfmulc2lem  19541  mbfmax  19543  mbfposr  19546  ismbf3d  19548  mbfaddlem  19554  mbfsup  19558  mbfinf  19559  i1f1lem  19583  i1fmulclem  19596  mbfi1fseqlem4  19612  itg2seq  19636  itg2monolem1  19644  itg2cnlem1  19655  itgfsum  19720  ditgneg  19746  limcdif  19765  limcnlp  19767  cnplimc  19776  rolle  19876  mvth  19878  dvne0  19897  lhop1lem  19899  itgsubst  19935  mdegle0  20002  deg1leb  20020  deg1le0  20036  q1peqb  20079  coemulhi  20174  dgrlt  20186  plydivlem3  20214  vieta1lem2  20230  aannenlem1  20247  ulmres  20306  reefiso  20366  pilem3  20371  ellogdm  20532  root1eq1  20641  angpieqvdlem  20671  angpieqvdlem2  20672  quad2  20681  1cubr  20684  quart  20703  rlimcnp  20806  wilthlem2  20854  sgmss  20891  isppw  20899  dvdsflip  20969  dvdsflsumcom  20975  fsumvma  20999  logfac2  21003  chpchtsum  21005  dchrmulcl  21035  dchreq  21044  dchrresb  21045  bclbnd  21066  bposlem1  21070  bposlem5  21074  lgsneg  21105  lgsquadlem1  21140  lgsquadlem2  21141  m1lgs  21148  dchrisumlem3  21187  dchrisum0lem1  21212  dfconngra1  21660  eupath2  21704  drngoi  21997  nmoreltpnf  22272  isblo2  22286  nmlnogt0  22300  phoeqi  22361  ubthlem2  22375  hire  22598  normgt0  22631  ho01i  23333  ho02i  23334  hoeq1  23335  hoeq2  23336  nmopreltpnf  23374  adjeq  23440  leop  23628  leopmul2i  23640  pjnormssi  23673  pjimai  23681  jplem1  23773  mddmd2  23814  mdslmd1lem1  23830  mdslmd1lem2  23831  superpos  23859  atnssm0  23881  dmdbr5ati  23927  feqmptdf  24077  ofpreima  24083  funcnv5mpt  24086  isoun  24091  xgepnf  24118  xlemnf  24119  iocinioc2  24144  xrdifh  24145  xdivmul  24173  isinftm  24253  isarchi2  24257  metidv  24289  pstmxmet  24294  sqsscirc2  24309  xrmulc1cn  24318  esumfsup  24462  1stmbfm  24612  2ndmbfm  24613  mbfmcnt  24620  ballotlemfc0  24752  ballotlemfcc  24753  ballotlemsima  24775  ballotlemfrcn0  24789  erdszelem7  24885  erdszelem9  24887  iscvm  24948  cvmlift3lem4  25011  zmodid2  25116  fprodss  25276  predfz  25480  sltval2  25613  axsegconlem6  25863  axeuclidlem  25903  axcontlem2  25906  axcontlem4  25908  axcontlem12  25916  fscgr  26016  seglelin  26052  btwnoutside  26061  lineunray  26083  nndivsub  26209  mblfinlem3  26247  mblfinlem4  26248  ismblfin  26249  itg2addnclem  26258  itg2addnclem2  26259  itg2gt0cn  26262  iblabsnclem  26270  ftc1anclem6  26287  areacirclem2  26295  areacirclem5  26298  areacirc  26299  cldbnd  26331  isfne4  26351  fneval  26369  filnetlem4  26412  cover2  26417  mettrifi  26465  prter3  26733  fz1eqin  26829  diophin  26833  dvdsabsmod0  27059  divalgmodcl  27060  jm2.19  27066  rmxdiophlem  27088  pw2f1ocnv  27110  wepwsolem  27118  elfilspd  27234  gicabl  27242  lindfmm  27276  islindf4  27287  islindf5  27288  sdrgacs  27488  idomodle  27491  isdomn3  27502  2reu4a  27945  dfdfat2  27973  funbrafv2b  28001  dfafn5a  28002  leaddsuble  28102  2submod  28163  frgra3v  28454  sbcoreleleq  28681  bnj1173  29433  islshpat  29877  lsatnle  29904  ellkr2  29951  lshpkr  29977  lkr0f2  30021  lduallkr3  30022  lkreqN  30030  cvrval2  30134  isat3  30167  glbconN  30236  hlrelat5N  30260  cvrval4N  30273  atlt  30296  1cvrco  30331  pmaple  30620  isline2  30633  isline4N  30636  elpaddn0  30659  elpadd2at2  30666  cdlemkid4  31793  dia0  31912  cdlemm10N  31978  dibglbN  32026  dihmeetlem4preN  32166  dochkrshp3  32248  dvh4dimlem  32303  lcfl5  32356  mapdpglem3  32535  mapdheq  32588  hdmap1eq  32662  hdmapval2lem  32694  hdmapoc  32794  hlhillcs  32821
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 179
  Copyright terms: Public domain W3C validator