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

Theorem 3bitr4g 279
Description: More general version of 3bitr4i 268. Useful for converting definitions in a formula. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
3bitr4g.1  |-  ( ph  ->  ( ps  <->  ch )
)
3bitr4g.2  |-  ( th  <->  ps )
3bitr4g.3  |-  ( ta  <->  ch )
Assertion
Ref Expression
3bitr4g  |-  ( ph  ->  ( th  <->  ta )
)

Proof of Theorem 3bitr4g
StepHypRef Expression
1 3bitr4g.2 . . 3  |-  ( th  <->  ps )
2 3bitr4g.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2syl5bb 248 . 2  |-  ( ph  ->  ( th  <->  ch )
)
4 3bitr4g.3 . 2  |-  ( ta  <->  ch )
53, 4syl6bbr 254 1  |-  ( ph  ->  ( th  <->  ta )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  bibi1d  310  pm5.32rd  621  orbi2d  682  orbi1d  683  3orbi123d  1251  3anbi123d  1252  xorbi12d  1306  hadbi123d  1372  cadbi123d  1373  cad1  1388  had0  1393  nfbidf  1754  drex1  1907  drnf1  1909  drnf2  1910  cbvexd  1949  drsb1  1962  sbal2  2073  eujustALT  2146  eubid  2150  mobid  2177  eqeq1  2289  eqeq2  2292  eleq1  2343  eleq2  2344  nfceqdf  2418  drnfc1  2435  drnfc2  2436  neeq1  2454  neeq2  2455  neleq1  2537  neleq2  2538  ralbida  2557  rexbida  2558  ralbidv2  2565  rexbidv2  2566  r19.21t  2628  r19.23t  2657  ralcom2  2704  reubida  2722  rmobida  2727  raleqf  2732  rexeqf  2733  reueq1f  2734  rmoeq1f  2735  cbvraldva2  2768  cbvrexdva2  2769  dfsbcq  2993  sbcbid  3044  sbcrext  3064  sbcabel  3068  sbnfc2  3141  psseq1  3263  psseq2  3264  ssconb  3309  uneq1  3322  ineq1  3363  difin2  3430  reuun2  3451  reldisj  3498  undif4  3511  disjssun  3512  pssdifcom1  3539  pssdifcom2  3540  sbcss  3564  eltpg  3676  raltpg  3684  rextpg  3685  intmin4  3891  dfiun2g  3935  iindif2  3971  iinin2  3972  disjprg  4019  disjxun  4021  breq  4025  breq1  4026  breq2  4027  treq  4119  opthg2  4247  oteqex2  4258  oteqex  4259  poeq1  4317  soeq1  4333  freq1  4363  weeq1  4381  weeq2  4382  ordeq  4399  limeq  4404  ordunisssuc  4495  reusv2lem5  4539  reusv5OLD  4544  reusv7OLD  4546  rexxfrd  4549  rexxfr2d  4551  rabxfrd  4555  iunpw  4570  tfinds  4650  opthprc  4736  wesn  4761  releq  4771  eqrel  4777  eqrelrel  4788  xpiindi  4821  brcnvg  4862  brresg  4963  resieq  4965  dmsnopg  5144  dfco2a  5173  iotaeq  5227  sniota  5246  imadif  5327  fneq1  5333  fneq2  5334  feq1  5375  feq2  5376  feq3  5377  f1eq1  5432  f1eq2  5433  f1eq3  5434  foeq1  5447  foeq2  5448  foeq3  5449  f1oeq1  5463  f1oeq2  5464  f1oeq3  5465  fun11iun  5493  mpteqb  5614  rexrnmpt  5670  dffo3  5675  fmptco  5691  dff13  5783  f1imaeq  5789  f1imapss  5790  cbvexfo  5800  f1eqcocnv  5805  fliftcnv  5810  isoeq1  5816  isoeq2  5817  isoeq3  5818  isoeq4  5819  isoeq5  5820  isomin  5834  isowe  5846  fnotovb  5894  mpt2eq123  5907  rexrnmpt2  5959  ottpos  6244  dmtpos  6246  opiota  6290  riotaeqdv  6305  onoviun  6360  smoeq  6367  smoiso2  6386  tfr2b  6412  oarec  6560  oeeui  6600  nnacan  6626  nnmcan  6632  ereq1  6667  ereq2  6668  elecg  6698  ereldm  6703  ixpiin  6842  boxriin  6858  boxcutc  6859  omxpenlem  6963  nnsdomo  7055  enfi  7079  isfinite2  7115  ixpfi2  7154  elfi2  7168  fipwss  7182  ennum  7580  cardsdom2  7621  aleph11  7711  alephiso  7725  fin23lem26  7951  compssiso  8000  isf34lem4  8003  isfin5-2  8017  fin1a2lem5  8030  brdom7disj  8156  brdom6disj  8157  fpwwe2lem8  8259  fpwwe2lem12  8263  fpwwe2lem13  8264  genpass  8633  ltasr  8722  axpre-lttri  8787  infm3  9713  creur  9740  eqreznegel  10303  rpneg  10383  ltxr  10457  icoshftf1o  10759  elfzm11  10853  nn0ennn  11041  nnesq  11225  hashbclem  11390  hashf1lem1  11393  leiso  11397  fz1isolem  11399  rexfiuz  11831  cau4  11840  ello1mpt2  11996  o1lo1  12011  fsumcom2  12237  incexc2  12297  bitsmod  12627  bitscmp  12629  smueqlem  12681  hashdvds  12843  prmreclem2  12964  vdwapun  13021  vdwmc2  13026  imasaddfnlem  13430  comfeq  13609  oppcsect  13676  funcres2b  13771  funcpropd  13774  fullpropd  13794  fthpropd  13795  fthres2b  13804  fthres2c  13805  fullres2c  13813  ffthres2c  13814  fucsect  13846  fucinv  13847  setcsect  13921  tosso  14142  pospropd  14238  odulatb  14247  oduclatb  14248  isipodrs  14264  odudlatb  14299  mndpropd  14398  mhmpropd  14421  issubm2  14426  grppropd  14500  grpinvcnv  14536  conjghm  14713  conjnmzb  14717  ghmpropd  14720  gapm  14760  cmnpropd  15098  ablpropd  15099  eqgabl  15131  gsumcom2  15226  dmdprd  15236  dprdw  15245  subgdmdprd  15269  pgpfac1lem2  15310  pgpfac1lem4  15313  rngpropd  15372  crngpropd  15373  crngunit  15444  unitpropd  15479  isnirred  15482  drngpropd  15539  fldpropd  15540  subrgpropd  15579  rhmpropd  15580  abvpropd  15607  lmodprop2d  15687  lsspropd  15774  lmhmpropd  15826  lbspropd  15852  lvecprop2d  15919  lvecpropd  15920  rrgsupp  16032  opprdomn  16042  fiidomfld  16049  assapropd  16067  psrbagconf1o  16120  mplmonmul  16208  phlpropd  16559  eltopspOLD  16656  istps2OLD  16659  tpspropd  16678  tgss2  16725  lmbr2  16989  ist1-2  17075  ist1-3  17077  subislly  17207  iskgen3  17244  txcnmpt  17318  hausdiag  17339  hauseqlcld  17340  xkococnlem  17353  tgqtop  17403  txhmeo  17494  uffix2  17619  ufildr  17626  txflf  17701  tgphaus  17799  divstgplem  17803  divstgphaus  17805  xpsdsval  17945  blin  17970  blres  17977  xmeterval  17978  xmspropd  18019  mspropd  18020  setsms  18026  metequiv  18055  ngppropd  18153  xrtgioo  18312  metdsge  18353  icopnfcnv  18440  iccpnfcnv  18442  lmhmclm  18584  lmmbr  18684  equivcmet  18741  cmspropd  18771  iunmbl2  18914  ioombl1lem4  18918  mbfaddlem  19015  i1fmullem  19049  itg1mulc  19059  iblcnlem1  19142  iblrelem  19145  iblre  19148  iblcn  19153  limcun  19245  mvth  19339  ofmulrt  19662  resinf1o  19898  quad2  20135  1cubr  20138  dcubic  20142  wilthlem2  20307  dvdsflip  20422  dvdsflf1o  20427  dvdsflsumcom  20428  fsumvma  20452  vmasum  20455  logfac2  20456  logfaclbnd  20461  dchrelbas3  20477  lgsquadlem1  20593  lgsquadlem2  20594  isass  20983  ocin  21875  chpsscon3  22082  chscllem2  22217  adjval  22470  pjimai  22756  mdsldmd1i  22911  elat2  22920  mdsymi  22991  rmoxfrdOLD  23146  rmoxfrd  23147  fmptcof2  23229  disjrdx  23370  eupath2lem2  23902  dfrtrclrec2  24040  dfpo2  24112  dfres3  24116  dfrdg4  24488  altopthbg  24502  ax5seg  24566  broutsideof3  24749  nabi1  24828  nabi2  24829  relrefcnv  25117  iscst4  25177  trinv  25395  svs3  25488  cnvtr  25616  dualded  25783  vtarsuelt  25895  istotbnd3  26495  sstotbnd  26499  heibor  26545  isidlc  26640  smprngopr  26677  mrefg2  26782  jm2.23  27089  wepwsolem  27138  dnwech  27145  islssfg2  27169  gicabl  27263  islindf4  27308  pmtrfrn  27400  acsfn1p  27507  isdomn3  27523  ralbidar  27648  rexbidar  27649  sbcrel  27979  sbcfun  27985  dfateq12d  27992  aov0nbovbi  28055  fnotaovb  28058  bnj919  28797  bnj956  28808  bnj976  28809  bnj1366  28862  bnj916  28965  islshpsm  29170  lcvexchlem1  29224  opcon1b  29388  isat3  29497  glbconN  29566  cdleme32fva  30626  cdlemg2cex  30780  dibelval3  31337  dib1dim  31355  doch11  31563  dochsordN  31564  mapdordlem1a  31824  mapd11  31829  mapdsord  31845  mapdcnv11N  31849  mapd0  31855
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