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  1766  drex1  1920  drnf1  1922  drnf2  1923  cbvexd  1962  drsb1  1975  sbal2  2086  eujustALT  2159  eubid  2163  mobid  2190  eqeq1  2302  eqeq2  2305  eleq1  2356  eleq2  2357  nfceqdf  2431  drnfc1  2448  drnfc2  2449  neeq1  2467  neeq2  2468  neleq1  2550  neleq2  2551  ralbida  2570  rexbida  2571  ralbidv2  2578  rexbidv2  2579  r19.21t  2641  r19.23t  2670  ralcom2  2717  reubida  2735  rmobida  2740  raleqf  2745  rexeqf  2746  reueq1f  2747  rmoeq1f  2748  cbvraldva2  2781  cbvrexdva2  2782  dfsbcq  3006  sbcbid  3057  sbcrext  3077  sbcabel  3081  sbnfc2  3154  psseq1  3276  psseq2  3277  ssconb  3322  uneq1  3335  ineq1  3376  difin2  3443  reuun2  3464  reldisj  3511  undif4  3524  disjssun  3525  pssdifcom1  3552  pssdifcom2  3553  sbcss  3577  eltpg  3689  raltpg  3697  rextpg  3698  intmin4  3907  dfiun2g  3951  iindif2  3987  iinin2  3988  disjprg  4035  disjxun  4037  breq  4041  breq1  4042  breq2  4043  treq  4135  opthg2  4263  oteqex2  4274  oteqex  4275  poeq1  4333  soeq1  4349  freq1  4379  weeq1  4397  weeq2  4398  ordeq  4415  limeq  4420  ordunisssuc  4511  reusv2lem5  4555  reusv5OLD  4560  reusv7OLD  4562  rexxfrd  4565  rexxfr2d  4567  rabxfrd  4571  iunpw  4586  tfinds  4666  opthprc  4752  wesn  4777  releq  4787  eqrel  4793  eqrelrel  4804  xpiindi  4837  brcnvg  4878  brresg  4979  resieq  4981  dmsnopg  5160  dfco2a  5189  iotaeq  5243  sniota  5262  imadif  5343  fneq1  5349  fneq2  5350  feq1  5391  feq2  5392  feq3  5393  f1eq1  5448  f1eq2  5449  f1eq3  5450  foeq1  5463  foeq2  5464  foeq3  5465  f1oeq1  5479  f1oeq2  5480  f1oeq3  5481  fun11iun  5509  mpteqb  5630  rexrnmpt  5686  dffo3  5691  fmptco  5707  dff13  5799  f1imaeq  5805  f1imapss  5806  cbvexfo  5816  f1eqcocnv  5821  fliftcnv  5826  isoeq1  5832  isoeq2  5833  isoeq3  5834  isoeq4  5835  isoeq5  5836  isomin  5850  isowe  5862  fnotovb  5910  mpt2eq123  5923  rexrnmpt2  5975  ottpos  6260  dmtpos  6262  opiota  6306  riotaeqdv  6321  onoviun  6376  smoeq  6383  smoiso2  6402  tfr2b  6428  oarec  6576  oeeui  6616  nnacan  6642  nnmcan  6648  ereq1  6683  ereq2  6684  elecg  6714  ereldm  6719  ixpiin  6858  boxriin  6874  boxcutc  6875  omxpenlem  6979  nnsdomo  7071  enfi  7095  isfinite2  7131  ixpfi2  7170  elfi2  7184  fipwss  7198  ennum  7596  cardsdom2  7637  aleph11  7727  alephiso  7741  fin23lem26  7967  compssiso  8016  isf34lem4  8019  isfin5-2  8033  fin1a2lem5  8046  brdom7disj  8172  brdom6disj  8173  fpwwe2lem8  8275  fpwwe2lem12  8279  fpwwe2lem13  8280  genpass  8649  ltasr  8738  axpre-lttri  8803  infm3  9729  creur  9756  eqreznegel  10319  rpneg  10399  ltxr  10473  icoshftf1o  10775  elfzm11  10869  nn0ennn  11057  nnesq  11241  hashbclem  11406  hashf1lem1  11409  leiso  11413  fz1isolem  11415  rexfiuz  11847  cau4  11856  ello1mpt2  12012  o1lo1  12027  fsumcom2  12253  incexc2  12313  bitsmod  12643  bitscmp  12645  smueqlem  12697  hashdvds  12859  prmreclem2  12980  vdwapun  13037  vdwmc2  13042  imasaddfnlem  13446  comfeq  13625  oppcsect  13692  funcres2b  13787  funcpropd  13790  fullpropd  13810  fthpropd  13811  fthres2b  13820  fthres2c  13821  fullres2c  13829  ffthres2c  13830  fucsect  13862  fucinv  13863  setcsect  13937  tosso  14158  pospropd  14254  odulatb  14263  oduclatb  14264  isipodrs  14280  odudlatb  14315  mndpropd  14414  mhmpropd  14437  issubm2  14442  grppropd  14516  grpinvcnv  14552  conjghm  14729  conjnmzb  14733  ghmpropd  14736  gapm  14776  cmnpropd  15114  ablpropd  15115  eqgabl  15147  gsumcom2  15242  dmdprd  15252  dprdw  15261  subgdmdprd  15285  pgpfac1lem2  15326  pgpfac1lem4  15329  rngpropd  15388  crngpropd  15389  crngunit  15460  unitpropd  15495  isnirred  15498  drngpropd  15555  fldpropd  15556  subrgpropd  15595  rhmpropd  15596  abvpropd  15623  lmodprop2d  15703  lsspropd  15790  lmhmpropd  15842  lbspropd  15868  lvecprop2d  15935  lvecpropd  15936  rrgsupp  16048  opprdomn  16058  fiidomfld  16065  assapropd  16083  psrbagconf1o  16136  mplmonmul  16224  phlpropd  16575  eltopspOLD  16672  istps2OLD  16675  tpspropd  16694  tgss2  16741  lmbr2  17005  ist1-2  17091  ist1-3  17093  subislly  17223  iskgen3  17260  txcnmpt  17334  hausdiag  17355  hauseqlcld  17356  xkococnlem  17369  tgqtop  17419  txhmeo  17510  uffix2  17635  ufildr  17642  txflf  17717  tgphaus  17815  divstgplem  17819  divstgphaus  17821  xpsdsval  17961  blin  17986  blres  17993  xmeterval  17994  xmspropd  18035  mspropd  18036  setsms  18042  metequiv  18071  ngppropd  18169  xrtgioo  18328  metdsge  18369  icopnfcnv  18456  iccpnfcnv  18458  lmhmclm  18600  lmmbr  18700  equivcmet  18757  cmspropd  18787  iunmbl2  18930  ioombl1lem4  18934  mbfaddlem  19031  i1fmullem  19065  itg1mulc  19075  iblcnlem1  19158  iblrelem  19161  iblre  19164  iblcn  19169  limcun  19261  mvth  19355  ofmulrt  19678  resinf1o  19914  quad2  20151  1cubr  20154  dcubic  20158  wilthlem2  20323  dvdsflip  20438  dvdsflf1o  20443  dvdsflsumcom  20444  fsumvma  20468  vmasum  20471  logfac2  20472  logfaclbnd  20477  dchrelbas3  20493  lgsquadlem1  20609  lgsquadlem2  20610  isass  20999  ocin  21891  chpsscon3  22098  chscllem2  22233  adjval  22486  pjimai  22772  mdsldmd1i  22927  elat2  22936  mdsymi  23007  rmoxfrdOLD  23162  rmoxfrd  23163  fmptcof2  23244  disjrdx  23385  eupath2lem2  23917  dfrtrclrec2  24055  dfpo2  24183  dfres3  24187  dfrdg4  24560  altopthbg  24574  ax5seg  24638  broutsideof3  24821  nabi1  24900  nabi2  24901  relrefcnv  25220  iscst4  25280  trinv  25498  svs3  25591  cnvtr  25719  dualded  25886  vtarsuelt  25998  istotbnd3  26598  sstotbnd  26602  heibor  26648  isidlc  26743  smprngopr  26780  mrefg2  26885  jm2.23  27192  wepwsolem  27241  dnwech  27248  islssfg2  27272  gicabl  27366  islindf4  27411  pmtrfrn  27503  acsfn1p  27610  isdomn3  27626  ralbidar  27751  rexbidar  27752  sbcrel  28084  sbcfun  28090  dfateq12d  28097  aov0nbovbi  28163  fnotaovb  28166  bnj919  29113  bnj956  29124  bnj976  29125  bnj1366  29178  bnj916  29281  drex1NEW7  29471  drnf1NEW7  29472  drnf2wAUX7  29475  drnf2w2AUX7  29478  drnf2w3AUX7  29481  drsb1NEW7  29483  drnf2OLD7  29670  cbvexdOLD7  29689  sbal2OLD7  29724  islshpsm  29792  lcvexchlem1  29846  opcon1b  30010  isat3  30119  glbconN  30188  cdleme32fva  31248  cdlemg2cex  31402  dibelval3  31959  dib1dim  31977  doch11  32185  dochsordN  32186  mapdordlem1a  32446  mapd11  32451  mapdsord  32467  mapdcnv11N  32471  mapd0  32477
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