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  2055  drnf1  2057  drnf2OLD  2059  drsb1  2102  sbal2  2210  eujustALT  2283  eubid  2287  mobid  2314  eqeq1  2441  eqeq2  2444  eleq1  2495  eleq2  2496  nfceqdf  2570  drnfc1  2587  drnfc2  2588  neeq1  2606  neeq2  2607  neleq1  2691  neleq2  2692  ralbida  2711  rexbida  2712  ralbidv2  2719  rexbidv2  2720  r19.21t  2783  r19.23t  2812  ralcom2  2864  reubida  2882  rmobida  2887  raleqf  2892  rexeqf  2893  reueq1f  2894  rmoeq1f  2895  cbvraldva2  2928  cbvrexdva2  2929  dfsbcq  3155  sbcbid  3206  sbcrext  3226  sbcabel  3230  sbnfc2  3301  psseq1  3426  psseq2  3427  ssconb  3472  uneq1  3486  ineq1  3527  difin2  3595  reuun2  3616  reldisj  3663  undif4  3676  disjssun  3677  pssdifcom1  3705  pssdifcom2  3706  sbcss  3730  eltpg  3843  raltpg  3851  rextpg  3852  intmin4  4071  dfiun2g  4115  iindif2  4152  iinin2  4153  disjprg  4200  disjxun  4202  breq  4206  breq1  4207  breq2  4208  treq  4300  opthg2  4429  oteqex2  4440  oteqex  4441  poeq1  4498  soeq1  4514  freq1  4544  weeq1  4562  weeq2  4563  ordeq  4580  limeq  4585  ordunisssuc  4676  reusv2lem5  4720  reusv5OLD  4725  reusv7OLD  4727  rexxfrd  4730  rexxfr2d  4732  rabxfrd  4736  iunpw  4751  tfinds  4831  opthprc  4917  wesn  4941  releq  4951  eqrel  4957  eqrelrel  4969  xpiindi  5002  brcnvg  5045  brresg  5146  resieq  5148  dmsnopg  5333  dfco2a  5362  iotaeq  5418  sniota  5437  imadif  5520  fneq1  5526  fneq2  5527  feq1  5568  feq2  5569  feq3  5570  f1eq1  5626  f1eq2  5627  f1eq3  5628  foeq1  5641  foeq2  5642  foeq3  5643  f1oeq1  5657  f1oeq2  5658  f1oeq3  5659  fun11iun  5687  mpteqb  5811  rexrnmpt  5871  dffo3  5876  fmptco  5893  dff13  5996  f1imaeq  6003  f1imapss  6004  cbvexfo  6015  f1eqcocnv  6020  fliftcnv  6025  isoeq1  6031  isoeq2  6032  isoeq3  6033  isoeq4  6034  isoeq5  6035  isomin  6049  isowe  6061  fnotovb  6109  mpt2eq123  6125  rexrnmpt2  6177  ottpos  6481  dmtpos  6483  opiota  6527  riotaeqdv  6542  onoviun  6597  smoeq  6604  smoiso2  6623  tfr2b  6649  oarec  6797  oeeui  6837  nnacan  6863  nnmcan  6869  ereq1  6904  ereq2  6905  elecg  6935  ereldm  6940  ixpiin  7080  boxriin  7096  boxcutc  7097  omxpenlem  7201  nnsdomo  7293  enfi  7317  isfinite2  7357  ixpfi2  7397  elfi2  7411  fipwss  7426  ennum  7826  cardsdom2  7867  aleph11  7957  alephiso  7971  fin23lem26  8197  compssiso  8246  isf34lem4  8249  isfin5-2  8263  fin1a2lem5  8276  brdom7disj  8401  brdom6disj  8402  fpwwe2lem8  8504  fpwwe2lem12  8508  fpwwe2lem13  8509  genpass  8878  ltasr  8967  axpre-lttri  9032  infm3  9959  creur  9986  eqreznegel  10553  rpneg  10633  ltxr  10707  icoshftf1o  11012  elfzm11  11108  nn0ennn  11310  nnesq  11495  hashbclem  11693  hashf1lem1  11696  leiso  11700  fz1isolem  11702  rexfiuz  12143  cau4  12152  ello1mpt2  12308  o1lo1  12323  fsumcom2  12550  incexc2  12610  bitsmod  12940  bitscmp  12942  smueqlem  12994  hashdvds  13156  prmreclem2  13277  vdwapun  13334  vdwmc2  13339  imasaddfnlem  13745  comfeq  13924  oppcsect  13991  funcres2b  14086  funcpropd  14089  fullpropd  14109  fthpropd  14110  fthres2b  14119  fthres2c  14120  fullres2c  14128  ffthres2c  14129  fucsect  14161  fucinv  14162  setcsect  14236  tosso  14457  pospropd  14553  odulatb  14562  oduclatb  14563  isipodrs  14579  odudlatb  14614  mndpropd  14713  mhmpropd  14736  issubm2  14741  grppropd  14815  grpinvcnv  14851  conjghm  15028  conjnmzb  15032  ghmpropd  15035  gapm  15075  cmnpropd  15413  ablpropd  15414  eqgabl  15446  gsumcom2  15541  dmdprd  15551  dprdw  15560  subgdmdprd  15584  pgpfac1lem2  15625  pgpfac1lem4  15628  rngpropd  15687  crngpropd  15688  crngunit  15759  unitpropd  15794  isnirred  15797  drngpropd  15854  fldpropd  15855  subrgpropd  15894  rhmpropd  15895  abvpropd  15922  lmodprop2d  15998  lsspropd  16085  lmhmpropd  16137  lbspropd  16163  lvecprop2d  16230  lvecpropd  16231  rrgsupp  16343  opprdomn  16353  fiidomfld  16360  assapropd  16378  psrbagconf1o  16431  mplmonmul  16519  phlpropd  16878  eltopspOLD  16975  istps2OLD  16978  tpspropd  16997  tgss2  17044  lmbr2  17315  ist1-2  17403  ist1-3  17405  subislly  17536  iskgen3  17573  txcnmpt  17648  hausdiag  17669  hauseqlcld  17670  xkococnlem  17683  tgqtop  17736  txhmeo  17827  uffix2  17948  ufildr  17955  txflf  18030  tgphaus  18138  divstgplem  18142  divstgphaus  18144  xpsdsval  18403  blin  18443  blres  18453  xmeterval  18454  xmspropd  18495  mspropd  18496  setsms  18502  metequiv  18531  metustsymOLD  18583  metustsym  18584  restmetu  18609  ngppropd  18670  xrtgioo  18829  metdsge  18871  icopnfcnv  18959  iccpnfcnv  18961  lmhmclm  19103  lmmbr  19203  equivcmet  19260  cmspropd  19294  iunmbl2  19443  ioombl1lem4  19447  mbfaddlem  19544  i1fmullem  19578  itg1mulc  19588  iblcnlem1  19671  iblrelem  19674  iblre  19677  iblcn  19682  limcun  19774  mvth  19868  ofmulrt  20191  resinf1o  20430  quad2  20671  1cubr  20674  dcubic  20678  wilthlem2  20844  dvdsflip  20959  dvdsflf1o  20964  dvdsflsumcom  20965  fsumvma  20989  vmasum  20992  logfac2  20993  logfaclbnd  20998  dchrelbas3  21014  lgsquadlem1  21130  lgsquadlem2  21131  eupath2lem2  21692  isass  21896  ocin  22790  chpsscon3  22997  chscllem2  23132  adjval  23385  pjimai  23671  mdsldmd1i  23826  elat2  23835  mdsymi  23906  rmoxfrdOLD  23971  rmoxfrd  23972  disjrdx  24023  fmptcof2  24068  funcnv5mpt  24076  1stpreima  24087  2ndpreima  24088  zhmnrg  24343  qqhval2  24358  dfrtrclrec2  25135  fprodcom2  25300  dfpo2  25370  dfres3  25374  sscoid  25750  dfrdg4  25787  altopthbg  25805  ax5seg  25869  broutsideof3  26052  ftc1anclem5  26274  istotbnd3  26471  sstotbnd  26475  heibor  26521  isidlc  26616  smprngopr  26653  mrefg2  26752  jm2.23  27058  wepwsolem  27107  dnwech  27114  islssfg2  27137  gicabl  27231  islindf4  27276  pmtrfrn  27368  acsfn1p  27475  isdomn3  27491  ralbidar  27615  rexbidar  27616  sbcrel  27948  sbcfun  27954  dfateq12d  27960  aov0nbovbi  28026  fnotaovb  28029  rexxfrd2  28060  elfzomelpfzo  28112  el2wlkonotot1  28294  2pthwlkonot  28305  usg2spot2nb  28391  bnj919  29073  bnj956  29084  bnj976  29085  bnj1366  29138  bnj916  29241  drex1NEW7  29431  drnf1NEW7  29432  drnf2wAUX7  29435  drnf2w2AUX7  29438  drnf2w3AUX7  29441  drsb1NEW7  29443  drnf2OLD7  29653  cbvexdOLD7  29672  sbal2OLD7  29705  islshpsm  29715  lcvexchlem1  29769  opcon1b  29933  isat3  30042  glbconN  30111  cdleme32fva  31171  cdlemg2cex  31325  dibelval3  31882  dib1dim  31900  doch11  32108  dochsordN  32109  mapdordlem1a  32369  mapd11  32374  mapdsord  32390  mapdcnv11N  32394  mapd0  32400
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