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

Theorem 3bitr4g 280
Description: More general version of 3bitr4i 269. 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 249 . 2  |-  ( ph  ->  ( th  <->  ch )
)
4 3bitr4g.3 . 2  |-  ( ta  <->  ch )
53, 4syl6bbr 255 1  |-  ( ph  ->  ( th  <->  ta )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  bibi1d  311  pm5.32rd  622  orbi2d  683  orbi1d  684  3orbi123d  1253  3anbi123d  1254  nanbi1  1304  nanbi2  1305  xorbi12d  1324  hadbi123d  1391  cadbi123d  1392  cad1  1407  had0  1412  nfbidf  1790  cbvexd  1988  drex1  2059  drnf1  2061  drnf2OLD  2063  drsb1  2112  sbal2  2211  eujustALT  2284  eubid  2288  mobid  2315  eqeq1  2442  eqeq2  2445  eleq1  2496  eleq2  2497  nfceqdf  2571  drnfc1  2588  drnfc2  2589  neeq1  2609  neeq2  2610  neleq1  2699  neleq2  2700  ralbida  2719  rexbida  2720  ralbidv2  2727  rexbidv2  2728  r19.21t  2791  r19.23t  2820  ralcom2  2872  reubida  2890  rmobida  2895  raleqf  2900  rexeqf  2901  reueq1f  2902  rmoeq1f  2903  cbvraldva2  2936  cbvrexdva2  2937  dfsbcq  3163  sbcbid  3214  sbcrext  3234  sbcabel  3238  sbnfc2  3309  psseq1  3434  psseq2  3435  ssconb  3480  uneq1  3494  ineq1  3535  difin2  3603  reuun2  3624  reldisj  3671  undif4  3684  disjssun  3685  pssdifcom1  3713  pssdifcom2  3714  sbcss  3738  eltpg  3851  raltpg  3859  rextpg  3860  intmin4  4079  dfiun2g  4123  iindif2  4160  iinin2  4161  disjprg  4208  disjxun  4210  breq  4214  breq1  4215  breq2  4216  treq  4308  opthg2  4437  oteqex2  4448  oteqex  4449  poeq1  4506  soeq1  4522  freq1  4552  weeq1  4570  weeq2  4571  ordeq  4588  limeq  4593  ordunisssuc  4684  reusv2lem5  4728  reusv5OLD  4733  reusv7OLD  4735  rexxfrd  4738  rexxfr2d  4740  rabxfrd  4744  iunpw  4759  tfinds  4839  opthprc  4925  wesn  4949  releq  4959  eqrel  4965  eqrelrel  4977  xpiindi  5010  brcnvg  5053  brresg  5154  resieq  5156  dmsnopg  5341  dfco2a  5370  iotaeq  5426  sniota  5445  imadif  5528  fneq1  5534  fneq2  5535  feq1  5576  feq2  5577  feq3  5578  f1eq1  5634  f1eq2  5635  f1eq3  5636  foeq1  5649  foeq2  5650  foeq3  5651  f1oeq1  5665  f1oeq2  5666  f1oeq3  5667  fun11iun  5695  mpteqb  5819  rexrnmpt  5879  dffo3  5884  fmptco  5901  dff13  6004  f1imaeq  6011  f1imapss  6012  cbvexfo  6023  f1eqcocnv  6028  fliftcnv  6033  isoeq1  6039  isoeq2  6040  isoeq3  6041  isoeq4  6042  isoeq5  6043  isomin  6057  isowe  6069  fnotovb  6117  mpt2eq123  6133  rexrnmpt2  6185  ottpos  6489  dmtpos  6491  opiota  6535  riotaeqdv  6550  onoviun  6605  smoeq  6612  smoiso2  6631  tfr2b  6657  oarec  6805  oeeui  6845  nnacan  6871  nnmcan  6877  ereq1  6912  ereq2  6913  elecg  6943  ereldm  6948  ixpiin  7088  boxriin  7104  boxcutc  7105  omxpenlem  7209  nnsdomo  7301  enfi  7325  isfinite2  7365  ixpfi2  7405  elfi2  7419  fipwss  7434  ennum  7834  cardsdom2  7875  aleph11  7965  alephiso  7979  fin23lem26  8205  compssiso  8254  isf34lem4  8257  isfin5-2  8271  fin1a2lem5  8284  brdom7disj  8409  brdom6disj  8410  fpwwe2lem8  8512  fpwwe2lem12  8516  fpwwe2lem13  8517  genpass  8886  ltasr  8975  axpre-lttri  9040  infm3  9967  creur  9994  eqreznegel  10561  rpneg  10641  ltxr  10715  icoshftf1o  11020  elfzm11  11116  nn0ennn  11318  nnesq  11503  hashbclem  11701  hashf1lem1  11704  leiso  11708  fz1isolem  11710  rexfiuz  12151  cau4  12160  ello1mpt2  12316  o1lo1  12331  fsumcom2  12558  incexc2  12618  bitsmod  12948  bitscmp  12950  smueqlem  13002  hashdvds  13164  prmreclem2  13285  vdwapun  13342  vdwmc2  13347  imasaddfnlem  13753  comfeq  13932  oppcsect  13999  funcres2b  14094  funcpropd  14097  fullpropd  14117  fthpropd  14118  fthres2b  14127  fthres2c  14128  fullres2c  14136  ffthres2c  14137  fucsect  14169  fucinv  14170  setcsect  14244  tosso  14465  pospropd  14561  odulatb  14570  oduclatb  14571  isipodrs  14587  odudlatb  14622  mndpropd  14721  mhmpropd  14744  issubm2  14749  grppropd  14823  grpinvcnv  14859  conjghm  15036  conjnmzb  15040  ghmpropd  15043  gapm  15083  cmnpropd  15421  ablpropd  15422  eqgabl  15454  gsumcom2  15549  dmdprd  15559  dprdw  15568  subgdmdprd  15592  pgpfac1lem2  15633  pgpfac1lem4  15636  rngpropd  15695  crngpropd  15696  crngunit  15767  unitpropd  15802  isnirred  15805  drngpropd  15862  fldpropd  15863  subrgpropd  15902  rhmpropd  15903  abvpropd  15930  lmodprop2d  16006  lsspropd  16093  lmhmpropd  16145  lbspropd  16171  lvecprop2d  16238  lvecpropd  16239  rrgsupp  16351  opprdomn  16361  fiidomfld  16368  assapropd  16386  psrbagconf1o  16439  mplmonmul  16527  phlpropd  16886  eltopspOLD  16983  istps2OLD  16986  tpspropd  17005  tgss2  17052  lmbr2  17323  ist1-2  17411  ist1-3  17413  subislly  17544  iskgen3  17581  txcnmpt  17656  hausdiag  17677  hauseqlcld  17678  xkococnlem  17691  tgqtop  17744  txhmeo  17835  uffix2  17956  ufildr  17963  txflf  18038  tgphaus  18146  divstgplem  18150  divstgphaus  18152  xpsdsval  18411  blin  18451  blres  18461  xmeterval  18462  xmspropd  18503  mspropd  18504  setsms  18510  metequiv  18539  metustsymOLD  18591  metustsym  18592  restmetu  18617  ngppropd  18678  xrtgioo  18837  metdsge  18879  icopnfcnv  18967  iccpnfcnv  18969  lmhmclm  19111  lmmbr  19211  equivcmet  19268  cmspropd  19302  iunmbl2  19451  ioombl1lem4  19455  mbfaddlem  19552  i1fmullem  19586  itg1mulc  19596  iblcnlem1  19679  iblrelem  19682  iblre  19685  iblcn  19690  limcun  19782  mvth  19876  ofmulrt  20199  resinf1o  20438  quad2  20679  1cubr  20682  dcubic  20686  wilthlem2  20852  dvdsflip  20967  dvdsflf1o  20972  dvdsflsumcom  20973  fsumvma  20997  vmasum  21000  logfac2  21001  logfaclbnd  21006  dchrelbas3  21022  lgsquadlem1  21138  lgsquadlem2  21139  eupath2lem2  21700  isass  21904  ocin  22798  chpsscon3  23005  chscllem2  23140  adjval  23393  pjimai  23679  mdsldmd1i  23834  elat2  23843  mdsymi  23914  rmoxfrdOLD  23979  rmoxfrd  23980  disjrdx  24031  fmptcof2  24076  funcnv5mpt  24084  1stpreima  24095  2ndpreima  24096  zhmnrg  24351  qqhval2  24366  dfrtrclrec2  25143  fprodcom2  25308  dfpo2  25378  dfres3  25382  sscoid  25758  dfrdg4  25795  altopthbg  25813  ax5seg  25877  broutsideof3  26060  ftc1anclem5  26284  istotbnd3  26480  sstotbnd  26484  heibor  26530  isidlc  26625  smprngopr  26662  mrefg2  26761  jm2.23  27067  wepwsolem  27116  dnwech  27123  islssfg2  27146  gicabl  27240  islindf4  27285  pmtrfrn  27377  acsfn1p  27484  isdomn3  27500  ralbidar  27624  rexbidar  27625  sbcrel  27957  sbcfun  27963  dfateq12d  27969  aov0nbovbi  28035  fnotaovb  28038  rexxfrd2  28073  elfzomelpfzo  28129  el2wlkonotot1  28341  2pthwlkonot  28352  usg2spot2nb  28454  bnj919  29136  bnj956  29147  bnj976  29148  bnj1366  29201  bnj916  29304  drex1NEW7  29494  drnf1NEW7  29495  drnf2wAUX7  29498  drnf2w2AUX7  29501  drnf2w3AUX7  29504  drsb1NEW7  29506  drnf2OLD7  29716  cbvexdOLD7  29735  sbal2OLD7  29768  islshpsm  29778  lcvexchlem1  29832  opcon1b  29996  isat3  30105  glbconN  30174  cdleme32fva  31234  cdlemg2cex  31388  dibelval3  31945  dib1dim  31963  doch11  32171  dochsordN  32172  mapdordlem1a  32432  mapd11  32437  mapdsord  32453  mapdcnv11N  32457  mapd0  32463
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 178
  Copyright terms: Public domain W3C validator