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  4035  ordsssuc  4495  reuhypd  4577  opbrop  4783  opelresiOLD  4982  opelresi  4983  iota1  5249  funbrfv2b  5583  dffn5  5584  dmfco  5609  fneqeql  5649  f1ompt  5698  dff13  5799  fliftcnv  5826  soisores  5840  isotr  5849  isoini  5851  caovord3  6049  releldm2  6186  brtpos  6259  tpostpos  6270  riota1  6339  riota2df  6341  riotasvdOLD  6364  oe1m  6559  oawordri  6564  oalimcl  6574  omlimcl  6592  omabs  6661  iserd  6702  qliftel  6757  qliftfun  6759  qliftf  6762  ecopovsym  6776  pw2f1olem  6982  mapen  7041  supisolem  7237  wemapso2  7283  cantnflem1  7407  mapfien  7415  wemapwe  7416  rankr1clem  7508  rankr1c  7509  ranklim  7532  r1pwOLD  7534  r1pwcl  7535  isfin1-2  8027  isfin1-4  8029  fin71num  8039  axdc3lem2  8093  ltmnq  8612  prlem936  8687  ltsosr  8732  ltasr  8738  xrlenlt  8906  ltxrlt  8909  letri3  8923  ne0gt0  8941  subadd  9070  ltsubadd2  9261  lesubadd2  9263  suble  9268  ltsub23  9270  ltaddpos2  9281  ltsubpos  9282  subge02  9305  ltord2  9318  leord2  9319  divmul  9443  divmul3  9445  rec11r  9475  ltdiv1  9636  ltdivmul2  9647  ledivmul2  9649  ltrec  9653  ltdiv2  9657  negiso  9746  infmrgelb  9750  infmrlb  9751  nnle1eq1  9790  avgle1  9967  avgle2  9968  avgle  9969  nn0le0eq0  10010  elz2  10056  znnnlt1  10066  zleltp1  10084  uzin  10276  difrp  10403  xrltlen  10496  dfle2  10497  xrletri3  10502  qbtwnre  10542  xltnegi  10559  supxrre  10662  supxrre1  10665  infmxrre  10670  ixxun  10688  elioo5  10724  elfz5  10806  elfzm11  10869  uzsplit  10871  flbi  10962  flbi2  10963  fznnfl  10982  lt2sq  11193  le2sq  11194  sqlecan  11225  bcval5  11346  shftfib  11583  mulre  11622  cnpart  11741  sqrlem6  11749  sqrmo  11753  elicc4abs  11819  abs2difabs  11834  cau4  11856  limsupgre  11971  clim2  11994  ello12  12006  ello1mpt2  12012  elo12  12017  lo1resb  12054  o1resb  12056  climeq  12057  climmpt2  12063  isercoll  12157  caucvgb  12168  fsumss  12214  fsumabs  12275  isumshft  12314  geomulcvg  12348  absefib  12494  xpnnenOLD  12504  dvdsval3  12551  dvdseq  12592  ndvdsadd  12623  bitscmp  12645  smupvallem  12690  dvdssq  12755  isprm3  12783  coprmdvds  12797  isprm5  12807  phiprmpw  12860  prmdiv  12869  pc11  12948  pcz  12949  pockthlem  12968  prmreclem2  12980  prmreclem4  12982  prmreclem6  12984  1arith  12990  vdwapun  13037  ramval  13071  rami  13078  ramcl  13092  pwsle  13407  ercpbllem  13466  invsym  13680  funcres2c  13791  latnle  14207  ismgmid  14403  grpinvcnv  14552  subgacs  14668  eqger  14683  gexdvds2  14912  pgpfi1  14922  pgpfi  14932  lsmass  14995  lssnle  14999  lsmdisj3b  15015  lsmhash  15030  ablsubadd  15129  gsumval3  15207  subgdmdprd  15285  pgpfac1lem2  15326  dvdsr02  15454  drngid2  15544  issubrg3  15589  lssacs  15740  lspsnel5  15768  psrbaglefi  16134  coe1mul2lem1  16360  prmirred  16464  chrdvds  16498  chrcong  16499  chrnzr  16500  znleval  16524  znleval2  16525  cygznlem3  16539  discld  16842  isneip  16858  lpdifsn  16891  restopnb  16922  restopn2  16924  restdis  16925  restperf  16930  lmbr2  17005  cncls2  17018  cnprest  17033  cnprest2  17034  iscnrm2  17082  ist0-2  17088  cnt0  17090  ist1-3  17093  ishaus2  17095  cmpfi  17151  dfcon2  17161  1stccnp  17204  1stccn  17205  subislly  17223  hausmapdom  17242  kgencn  17267  tx1cn  17319  tx2cn  17320  txcnmpt  17334  txrest  17341  hauseqlcld  17356  tgqtop  17419  qtopcld  17420  qtopcn  17421  ordthmeolem  17508  trfil2  17598  trfil3  17599  trnei  17603  ufildr  17642  fmfg  17660  rnelfm  17664  fmfnfm  17669  elflim  17682  fbflim  17687  flimrest  17694  isflf  17704  cnflf  17713  cnflf2  17714  fclscf  17736  cnfcf  17753  ptcmplem2  17763  ghmcnp  17813  tsmssubm  17841  xmetgt0  17938  prdsxmetlem  17948  elbl2  17966  blcom  17968  xblpnf  17969  blpnf  17970  xmeter  17995  setsxms  18041  imasf1obl  18050  stdbdbl  18079  metrest  18086  metcn  18105  txmetcn  18110  dscopn  18112  xrtgioo  18328  metdstri  18371  cncffvrn  18418  cnmpt2pc  18442  iihalf2  18447  icopnfhmeo  18457  evth2  18474  lmmbr3  18702  iscau3  18720  lmclimf  18745  metcld  18747  srabn  18793  minveclem4  18812  evthicc2  18836  ovolfioo  18843  ovolficc  18844  ovolgelb  18855  ovoliun  18880  shft2rab  18883  ovolshftlem1  18884  sca2rab  18887  ovolscalem1  18888  ismbl2  18902  ioombl1lem4  18934  mbfmulc2lem  19018  mbfmax  19020  mbfposr  19023  ismbf3d  19025  mbfaddlem  19031  mbfsup  19035  mbfinf  19036  i1f1lem  19060  i1fmulclem  19073  mbfi1fseqlem4  19089  itg2seq  19113  itg2monolem1  19121  itg2cnlem1  19132  itgfsum  19197  ditgneg  19223  limcdif  19242  limcnlp  19244  cnplimc  19253  rolle  19353  mvth  19355  dvne0  19374  lhop1lem  19376  itgsubst  19412  mdegle0  19479  deg1leb  19497  deg1le0  19513  q1peqb  19556  coemulhi  19651  dgrlt  19663  plydivlem3  19691  vieta1lem2  19707  aannenlem1  19724  ulmres  19783  reefiso  19840  pilem3  19845  ellogdm  20002  root1eq1  20111  angpieqvdlem  20141  angpieqvdlem2  20142  quad2  20151  1cubr  20154  quart  20173  rlimcnp  20276  wilthlem2  20323  sgmss  20360  isppw  20368  dvdsflip  20438  dvdsflsumcom  20444  fsumvma  20468  fsumvma2  20469  logfac2  20472  chpchtsum  20474  dchrmulcl  20504  dchreq  20513  dchrresb  20514  bclbnd  20535  bposlem1  20539  bposlem5  20543  lgsneg  20574  lgsquadlem1  20609  lgsquadlem2  20610  m1lgs  20617  dchrisumlem3  20656  dchrisum0lem1  20681  drngoi  21090  nmoreltpnf  21363  isblo2  21377  nmlnogt0  21391  phoeqi  21452  ubthlem2  21466  hire  21689  normgt0  21722  ho01i  22424  ho02i  22425  hoeq1  22426  hoeq2  22427  nmopreltpnf  22465  adjeq  22531  leop  22719  leopmul2i  22731  pjnormssi  22764  pjimai  22772  jplem1  22864  mddmd2  22905  mdslmd1lem1  22921  mdslmd1lem2  22922  superpos  22950  atnssm0  22972  dmdbr5ati  23018  ballotlemfc0  23067  ballotlemfcc  23068  ballotlemsima  23090  ballotlemfrcn0  23104  xdivmul  23124  xgtpnf  23130  feqmptdf  23243  funcnv5mpt  23251  isoun  23257  iocinioc2  23287  xrdifh  23288  sqsscirc2  23308  xrmulc1cn  23318  1stmbfm  23580  2ndmbfm  23581  mbfmcnt  23588  erdszelem7  23743  erdszelem9  23745  iscvm  23805  cvmlift3lem4  23868  eupath2  23919  zmodid2  24025  predfz  24274  sltval2  24381  dffun10  24524  axsegconlem6  24622  axeuclidlem  24662  axcontlem2  24665  axcontlem4  24667  axcontlem12  24675  fscgr  24775  seglelin  24811  btwnoutside  24820  lineunray  24842  nndivsub  24968  itg2addnclem  25003  itg2addnclem2  25004  itg2gt0cn  25006  itgaddnclem2  25010  iblabsnclem  25014  areacirclem4  25030  areacirclem6  25033  areacirc  25034  iscst4  25280  subaddv  25774  cldbnd  26347  isfne4  26372  fneval  26390  filnetlem4  26433  cover2  26461  mettrifi  26576  prter3  26853  fz1eqin  26951  diophin  26955  dvdsabsmod0  27182  divalgmodcl  27183  jm2.19  27189  rmxdiophlem  27211  pw2f1ocnv  27233  wepwsolem  27241  elfilspd  27358  gicabl  27366  lindfmm  27400  islindf4  27411  islindf5  27412  sdrgacs  27612  idomodle  27615  isdomn3  27626  2reu4a  28070  dfdfat2  28099  funbrafv2b  28127  dfafn5a  28128  frgra3v  28426  sbcoreleleq  28597  bnj1173  29348  islshpat  29829  lsatnle  29856  ellkr2  29903  lshpkr  29929  lkr0f2  29973  lduallkr3  29974  lkreqN  29982  cvrval2  30086  isat3  30119  glbconN  30188  hlrelat5N  30212  cvrval4N  30225  atlt  30248  1cvrco  30283  pmaple  30572  isline2  30585  isline4N  30588  elpaddn0  30611  elpadd2at2  30618  cdlemkid4  31745  dia0  31864  cdlemm10N  31930  dibglbN  31978  dihmeetlem4preN  32118  dochkrshp3  32200  dvh4dimlem  32255  lcfl5  32308  mapdpglem3  32487  mapdheq  32540  hdmap1eq  32614  hdmapval2lem  32646  hdmapoc  32746  hlhillcs  32773
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