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  1756  drex1  1910  drnf1  1912  drnf2  1913  cbvexd  1954  drsb1  1967  sbal2  2076  eujustALT  2147  eubid  2151  mobid  2178  eqeq1  2290  eqeq2  2293  eleq1  2344  eleq2  2345  nfceqdf  2419  drnfc1  2436  drnfc2  2437  neeq1  2455  neeq2  2456  neleq1  2538  neleq2  2539  ralbida  2558  rexbida  2559  ralbidv2  2566  rexbidv2  2567  r19.21t  2629  r19.23t  2658  ralcom2  2705  reubida  2723  rmobida  2728  raleqf  2733  rexeqf  2734  reueq1f  2735  rmoeq1f  2736  cbvraldva2  2769  cbvrexdva2  2770  dfsbcq  2994  sbcbid  3045  sbcrext  3065  sbcabel  3069  sbnfc2  3142  psseq1  3264  psseq2  3265  ssconb  3310  uneq1  3323  ineq1  3364  difin2  3431  reuun2  3452  reldisj  3499  undif4  3512  disjssun  3513  pssdifcom1  3540  pssdifcom2  3541  sbcss  3565  eltpg  3677  raltpg  3685  rextpg  3686  intmin4  3892  dfiun2g  3936  iindif2  3972  iinin2  3973  disjprg  4020  disjxun  4022  breq  4026  breq1  4027  breq2  4028  treq  4120  opthg2  4246  oteqex2  4257  oteqex  4258  poeq1  4316  soeq1  4332  freq1  4362  weeq1  4380  weeq2  4381  ordeq  4398  limeq  4403  ordunisssuc  4494  reusv2lem5  4538  reusv5OLD  4543  reusv7OLD  4545  rexxfrd  4548  rexxfr2d  4550  rabxfrd  4554  iunpw  4569  tfinds  4649  opthprc  4735  wesn  4760  releq  4770  eqrel  4776  eqrelrel  4787  xpiindi  4820  brcnvg  4861  brresg  4962  resieq  4964  dmsnopg  5142  dfco2a  5171  imadif  5293  fneq1  5299  fneq2  5300  feq1  5341  feq2  5342  feq3  5343  f1eq1  5398  f1eq2  5399  f1eq3  5400  foeq1  5413  foeq2  5414  foeq3  5415  f1oeq1  5429  f1oeq2  5430  f1oeq3  5431  fun11iun  5459  fv2  5482  mpteqb  5576  rexrnmpt  5632  dffo3  5637  fmptco  5653  dff13  5745  f1imaeq  5751  f1imapss  5752  cbvexfo  5762  f1eqcocnv  5767  fliftcnv  5772  isoeq1  5778  isoeq2  5779  isoeq3  5780  isoeq4  5781  isoeq5  5782  isomin  5796  isowe  5808  fnotovb  5856  mpt2eq123  5869  rexrnmpt2  5921  ottpos  6206  dmtpos  6208  iotaeq  6261  sniota  6280  opiota  6284  riotaeqdv  6301  onoviun  6356  smoeq  6363  smoiso2  6382  tfr2b  6408  oarec  6556  oeeui  6596  nnacan  6622  nnmcan  6628  ereq1  6663  ereq2  6664  elecg  6694  ereldm  6699  ixpiin  6838  boxriin  6854  boxcutc  6855  omxpenlem  6959  nnsdomo  7051  enfi  7075  isfinite2  7111  ixpfi2  7150  elfi2  7164  fipwss  7178  ennum  7576  cardsdom2  7617  aleph11  7707  alephiso  7721  fin23lem26  7947  compssiso  7996  isf34lem4  7999  isfin5-2  8013  fin1a2lem5  8026  brdom7disj  8152  brdom6disj  8153  fpwwe2lem8  8255  fpwwe2lem12  8259  fpwwe2lem13  8260  genpass  8629  ltasr  8718  axpre-lttri  8783  infm3  9709  creur  9736  eqreznegel  10299  rpneg  10379  ltxr  10453  icoshftf1o  10755  elfzm11  10849  nn0ennn  11037  nnesq  11221  hashbclem  11386  hashf1lem1  11389  leiso  11393  fz1isolem  11395  rexfiuz  11827  cau4  11836  ello1mpt2  11992  o1lo1  12007  fsumcom2  12233  incexc2  12293  bitsmod  12623  bitscmp  12625  smueqlem  12677  hashdvds  12839  prmreclem2  12960  vdwapun  13017  vdwmc2  13022  imasaddfnlem  13426  comfeq  13605  oppcsect  13672  funcres2b  13767  funcpropd  13770  fullpropd  13790  fthpropd  13791  fthres2b  13800  fthres2c  13801  fullres2c  13809  ffthres2c  13810  fucsect  13842  fucinv  13843  setcsect  13917  tosso  14138  pospropd  14234  odulatb  14243  oduclatb  14244  isipodrs  14260  odudlatb  14295  mndpropd  14394  mhmpropd  14417  issubm2  14422  grppropd  14496  grpinvcnv  14532  conjghm  14709  conjnmzb  14713  ghmpropd  14716  gapm  14756  cmnpropd  15094  ablpropd  15095  eqgabl  15127  gsumcom2  15222  dmdprd  15232  dprdw  15241  subgdmdprd  15265  pgpfac1lem2  15306  pgpfac1lem4  15309  rngpropd  15368  crngpropd  15369  crngunit  15440  unitpropd  15475  isnirred  15478  drngpropd  15535  fldpropd  15536  subrgpropd  15575  rhmpropd  15576  abvpropd  15603  lmodprop2d  15683  lsspropd  15770  lmhmpropd  15822  lbspropd  15848  lvecprop2d  15915  lvecpropd  15916  rrgsupp  16028  opprdomn  16038  fiidomfld  16045  assapropd  16063  psrbagconf1o  16116  mplmonmul  16204  phlpropd  16555  eltopspOLD  16652  istps2OLD  16655  tpspropd  16674  tgss2  16721  lmbr2  16985  ist1-2  17071  ist1-3  17073  subislly  17203  iskgen3  17240  txcnmpt  17314  hausdiag  17335  hauseqlcld  17336  xkococnlem  17349  tgqtop  17399  txhmeo  17490  uffix2  17615  ufildr  17622  txflf  17697  tgphaus  17795  divstgplem  17799  divstgphaus  17801  xpsdsval  17941  blin  17966  blres  17973  xmeterval  17974  xmspropd  18015  mspropd  18016  setsms  18022  metequiv  18051  ngppropd  18149  xrtgioo  18308  metdsge  18349  icopnfcnv  18436  iccpnfcnv  18438  lmhmclm  18580  lmmbr  18680  equivcmet  18737  cmspropd  18767  iunmbl2  18910  ioombl1lem4  18914  mbfaddlem  19011  i1fmullem  19045  itg1mulc  19055  iblcnlem1  19138  iblrelem  19141  iblre  19144  iblcn  19149  limcun  19241  mvth  19335  ofmulrt  19658  resinf1o  19894  quad2  20131  1cubr  20134  dcubic  20138  wilthlem2  20303  dvdsflip  20418  dvdsflf1o  20423  dvdsflsumcom  20424  fsumvma  20448  vmasum  20451  logfac2  20452  logfaclbnd  20457  dchrelbas3  20473  lgsquadlem1  20589  lgsquadlem2  20590  isass  20977  ocin  21871  chpsscon3  22078  chscllem2  22213  adjval  22466  pjimai  22752  mdsldmd1i  22907  elat2  22916  mdsymi  22987  eupath2lem2  23309  dfrtrclrec2  23447  dfpo2  23518  dfres3  23522  dfrdg4  23898  altopthbg  23912  ax5seg  23976  broutsideof3  24159  nabi1  24238  nabi2  24239  relrefcnv  24528  iscst4  24588  trinv  24806  svs3  24899  cnvtr  25027  dualded  25194  vtarsuelt  25306  istotbnd3  25906  sstotbnd  25910  heibor  25956  isidlc  26051  smprngopr  26088  mrefg2  26193  jm2.23  26500  wepwsolem  26549  dnwech  26556  islssfg2  26580  gicabl  26674  islindf4  26719  pmtrfrn  26811  acsfn1p  26918  isdomn3  26934  ralbidar  27059  rexbidar  27060  sbcrel  27370  sbcfun  27376  dfateq12d  27383  aov0nbovbi  27446  fnotaovb  27449  bnj919  28076  bnj956  28087  bnj976  28088  bnj1366  28141  bnj916  28244  islshpsm  28449  lcvexchlem1  28503  opcon1b  28667  isat3  28776  glbconN  28845  cdleme32fva  29905  cdlemg2cex  30059  dibelval3  30616  dib1dim  30634  doch11  30842  dochsordN  30843  mapdordlem1a  31103  mapd11  31108  mapdsord  31124  mapdcnv11N  31128  mapd0  31134
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