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

Theorem 3bitr4g 288
Description: More general version of 3bitr4i 277. 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 257 . 2  |-  ( ph  ->  ( th  <->  ch )
)
4 3bitr4g.3 . 2  |-  ( ta  <->  ch )
53, 4syl6bbr 263 1  |-  ( ph  ->  ( th  <->  ta )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185
This theorem is referenced by:  bibi1d  319  pm5.32rd  633  orbi2d  694  orbi1d  695  3orbi123d  1281  3anbi123d  1282  nanbi1  1334  nanbi2  1335  xorbi12d  1357  hadbi123d  1426  cadbi123d  1427  cad1  1443  had0  1448  nfbidf  1819  cbvexd  1973  drex1  2018  drnf1  2020  drsb1  2065  sbal2OLD  2185  eujustALT  2257  eubid  2272  mobid  2273  eqeq1  2439  eqeq2  2442  eleq1  2493  eleq2  2494  nfceqdf  2568  drnfc1  2585  drnfc2  2586  neeq1  2606  neeq2  2607  neleq1  2699  neleq2  2700  ralbida  2719  rexbida  2720  ralbidv2  2727  rexbidv2  2728  r19.21t  2791  r19.23t  2821  ralcom2  2875  reubida  2893  rmobida  2898  raleqf  2903  rexeqf  2904  reueq1f  2905  rmoeq1f  2906  cbvraldva2  2941  cbvrexdva2  2942  dfsbcq  3177  sbcbid  3232  sbcrextOLD  3256  sbcrext  3257  sbcabel  3263  psseq1  3431  psseq2  3432  ssconb  3477  uneq1  3491  ineq1  3533  difin2  3600  reuun2  3621  sbcnel12g  3666  sbnfc2  3694  reldisj  3710  undif4  3723  disjssun  3724  pssdifcom1  3752  pssdifcom2  3753  sbcssg  3778  eltpg  3906  raltpg  3915  rextpg  3916  intmin4  4145  dfiun2g  4190  iindif2  4227  iinin2  4228  disjprg  4276  disjxun  4278  breq  4282  breq1  4283  breq2  4284  treq  4379  reusv2lem5  4485  reusv5OLD  4490  reusv7OLD  4492  rexxfrd  4495  rexxfr2d  4497  rabxfrd  4501  opthg2  4557  oteqex2  4571  oteqex  4572  poeq1  4631  soeq1  4647  freq1  4677  weeq1  4695  weeq2  4696  ordeq  4713  limeq  4718  ordunisssuc  4808  opthprc  4873  wesn  4897  releq  4909  sbcrel  4913  eqrel  4916  eqrelrel  4928  xpiindi  4962  brcnvg  5007  brresg  5106  resieq  5108  dmsnopg  5298  dfco2a  5326  iotaeq  5377  sniota  5396  sbcfung  5429  imadif  5481  fneq1  5487  fneq2  5488  feq1  5530  feq2  5531  feq3  5532  sbcfng  5544  sbcfg  5545  f1eq1  5589  f1eq2  5590  f1eq3  5591  foeq1  5604  foeq2  5605  foeq3  5606  f1oeq1  5620  f1oeq2  5621  f1oeq3  5622  mpteqb  5776  rexrnmpt  5841  dffo3  5846  fmptco  5863  dff13  5958  f1imaeq  5965  f1imapss  5966  cbvexfo  5981  f1eqcocnv  5986  fliftcnv  5991  isoeq1  5997  isoeq2  5998  isoeq3  5999  isoeq4  6000  isoeq5  6001  isomin  6015  isowe  6027  fnotovb  6118  mpt2eq123  6134  rexrnmpt2  6195  iunpw  6379  tfinds  6459  fun11iun  6526  opiota  6622  ottpos  6744  dmtpos  6746  onoviun  6790  smoeq  6797  smoiso2  6816  tfr2b  6841  oarec  6989  oeeui  7029  nnacan  7055  nnmcan  7061  ereq1  7096  ereq2  7097  elecg  7127  ereldm  7132  ixpiin  7277  boxriin  7293  boxcutc  7294  omxpenlem  7400  nnsdomo  7493  enfi  7517  isfinite2  7558  ixpfi2  7597  elfi2  7652  fipwss  7667  ennum  8105  cardsdom2  8146  aleph11  8242  alephiso  8256  fin23lem26  8482  compssiso  8531  isf34lem4  8534  isfin5-2  8548  fin1a2lem5  8561  brdom7disj  8686  brdom6disj  8687  fpwwe2lem8  8791  fpwwe2lem12  8795  fpwwe2lem13  8796  genpass  9165  ltasr  9254  axpre-lttri  9319  infm3  10276  creur  10303  eqreznegel  10927  rpneg  11007  ltxr  11082  icoshftf1o  11394  elfzm11  11511  elfzomelpfzo  11612  nn0ennn  11784  nnesq  11971  pr2pwpr  12166  hashbclem  12188  hashf1lem1  12191  leiso  12195  fz1isolem  12197  repsdf2  12399  rexfiuz  12818  cau4  12827  ello1mpt2  12983  o1lo1  12998  fsumcom2  13224  incexc2  13283  bitsmod  13614  bitscmp  13616  smueqlem  13668  hashdvds  13832  prmreclem2  13960  vdwapun  14017  vdwmc2  14022  imasaddfnlem  14448  comfeq  14627  oppcsect  14694  funcres2b  14789  funcpropd  14792  fullpropd  14812  fthpropd  14813  fthres2b  14822  fthres2c  14823  fullres2c  14831  ffthres2c  14832  fucsect  14864  fucinv  14865  setcsect  14939  tosso  15188  pospropd  15286  odulatb  15295  oduclatb  15296  isipodrs  15313  odudlatb  15348  mndpropd  15428  mhmpropd  15452  issubm2  15457  grppropd  15535  grpinvcnv  15573  conjghm  15756  conjnmzb  15760  ghmpropd  15763  gapm  15803  symg1bas  15880  pmtrfrn  15943  cmnpropd  16265  ablpropd  16266  eqgabl  16298  gsumcom2  16440  dmdprd  16453  dprdw  16467  dprdwOLD  16473  subgdmdprd  16504  pgpfac1lem2  16549  pgpfac1lem4  16552  rngpropd  16611  crngpropd  16612  crngunit  16687  unitpropd  16722  isnirred  16725  drngpropd  16782  fldpropd  16783  subrgpropd  16822  rhmpropd  16823  abvpropd  16850  lmodprop2d  16930  lsspropd  17019  lmhmpropd  17075  lbspropd  17101  lvecprop2d  17168  lvecpropd  17169  rrgsuppOLD  17284  opprdomn  17294  fiidomfld  17301  assapropd  17319  psrbagconf1o  17377  mplmonmul  17476  phlpropd  17925  eltopspOLD  18364  istps2OLD  18367  tpspropd  18386  tgss2  18433  lmbr2  18704  ist1-2  18792  ist1-3  18794  subislly  18926  iskgen3  18963  txcnmpt  19038  hausdiag  19059  hauseqlcld  19060  xkococnlem  19073  tgqtop  19126  txhmeo  19217  uffix2  19338  ufildr  19345  txflf  19420  tgphaus  19528  divstgplem  19532  divstgphaus  19534  xpsdsval  19797  blin  19837  blres  19847  xmeterval  19848  xmspropd  19889  mspropd  19890  setsms  19896  metequiv  19925  metustsymOLD  19977  metustsym  19978  restmetu  20003  ngppropd  20064  xrtgioo  20224  metdsge  20266  icopnfcnv  20355  iccpnfcnv  20357  lmhmclm  20499  lmmbr  20610  equivcmet  20667  cmspropd  20701  iunmbl2  20879  ioombl1lem4  20883  mbfaddlem  20979  i1fmullem  21013  itg1mulc  21023  iblcnlem1  21106  iblrelem  21109  iblre  21112  iblcn  21117  limcun  21211  mvth  21305  ofmulrt  21632  resinf1o  21876  quad2  22118  1cubr  22121  dcubic  22125  wilthlem2  22291  dvdsflip  22406  dvdsflf1o  22411  dvdsflsumcom  22412  fsumvma  22436  vmasum  22439  logfac2  22440  logfaclbnd  22445  dchrelbas3  22461  lgsquadlem1  22577  lgsquadlem2  22578  ax5seg  23006  eupath2lem2  23421  isass  23625  ocin  24521  chpsscon3  24728  chscllem2  24863  adjval  25116  pjimai  25402  mdsldmd1i  25557  elat2  25566  mdsymi  25637  sbceqbid  25687  sbceqbidf  25688  rmoxfrdOLD  25699  rmoxfrd  25700  disjrdx  25756  eqrelrd2  25769  fmptcof2  25802  funcnv5mpt  25811  1stpreima  25824  2ndpreima  25825  fpwrelmapffslem  25856  zhmnrg  26249  qqhval2  26264  dfrtrclrec2  27191  fprodcom2  27341  dfpo2  27411  dfres3  27415  sscoid  27790  dfrdg4  27827  altopthbg  27845  broutsideof3  28003  wl-sb8eut  28239  wl-sb8mot  28240  ftc1anclem5  28312  istotbnd3  28511  sstotbnd  28515  heibor  28561  isidlc  28656  smprngopr  28693  mrefg2  28885  jm2.23  29187  wepwsolem  29236  dnwech  29243  islssfg2  29266  gicabl  29296  acsfn1p  29398  isdomn3  29414  ralbidar  29543  rexbidar  29544  dfateq12d  29878  aov0nbovbi  29944  fnotaovb  29947  rexxfrd2  29981  el2wlkonotot1  30236  2pthwlkonot  30247  Lemma2  30336  rusgranumwlkb0  30414  usg2spot2nb  30501  numclwwlkovfel2  30519  lindslinindsimp2lem5  30702  trsbc  30945  bnj919  31459  bnj956  31469  bnj976  31470  bnj1366  31522  bnj916  31625  bj-nfbi  31817  bj-cbvexdv  31865  bj-drex1v  31890  bj-drnf1v  31891  bj-eleq1w  31967  islshpsm  32195  lcvexchlem1  32249  opcon1b  32413  isat3  32522  glbconN  32591  cdleme32fva  33651  cdlemg2cex  33805  dibelval3  34362  dib1dim  34380  doch11  34588  dochsordN  34589  mapdordlem1a  34849  mapd11  34854  mapdsord  34870  mapdcnv11N  34874  mapd0  34880
  Copyright terms: Public domain W3C validator