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

Theorem 3bitr4g 281
Description: More general version of 3bitr4i 270. 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 250 . 2  |-  ( ph  ->  ( th  <->  ch )
)
4 3bitr4g.3 . 2  |-  ( ta  <->  ch )
53, 4syl6bbr 256 1  |-  ( ph  ->  ( th  <->  ta )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178
This theorem is referenced by:  bibi1d  312  pm5.32rd  623  orbi2d  684  orbi1d  685  3orbi123d  1254  3anbi123d  1255  nanbi1  1305  nanbi2  1306  xorbi12d  1325  hadbi123d  1392  cadbi123d  1393  cad1  1408  had0  1413  nfbidf  1791  cbvexd  1989  drex1  2060  drnf1  2062  drnf2OLD  2064  drsb1  2114  sbal2  2213  eujustALT  2286  eubid  2290  mobid  2317  eqeq1  2444  eqeq2  2447  eleq1  2498  eleq2  2499  nfceqdf  2573  drnfc1  2590  drnfc2  2591  neeq1  2611  neeq2  2612  neleq1  2701  neleq2  2702  ralbida  2721  rexbida  2722  ralbidv2  2729  rexbidv2  2730  r19.21t  2793  r19.23t  2822  ralcom2  2874  reubida  2892  rmobida  2897  raleqf  2902  rexeqf  2903  reueq1f  2904  rmoeq1f  2905  cbvraldva2  2938  cbvrexdva2  2939  dfsbcq  3165  sbcbid  3216  sbcrext  3236  sbcabel  3240  sbnfc2  3311  psseq1  3436  psseq2  3437  ssconb  3482  uneq1  3496  ineq1  3537  difin2  3605  reuun2  3626  reldisj  3673  undif4  3686  disjssun  3687  pssdifcom1  3715  pssdifcom2  3716  sbcss  3740  eltpg  3853  raltpg  3861  rextpg  3862  intmin4  4081  dfiun2g  4125  iindif2  4162  iinin2  4163  disjprg  4211  disjxun  4213  breq  4217  breq1  4218  breq2  4219  treq  4311  opthg2  4440  oteqex2  4451  oteqex  4452  poeq1  4509  soeq1  4525  freq1  4555  weeq1  4573  weeq2  4574  ordeq  4591  limeq  4596  ordunisssuc  4687  reusv2lem5  4731  reusv5OLD  4736  reusv7OLD  4738  rexxfrd  4741  rexxfr2d  4743  rabxfrd  4747  iunpw  4762  tfinds  4842  opthprc  4928  wesn  4952  releq  4962  eqrel  4968  eqrelrel  4980  xpiindi  5013  brcnvg  5056  brresg  5157  resieq  5159  dmsnopg  5344  dfco2a  5373  iotaeq  5429  sniota  5448  imadif  5531  fneq1  5537  fneq2  5538  feq1  5579  feq2  5580  feq3  5581  f1eq1  5637  f1eq2  5638  f1eq3  5639  foeq1  5652  foeq2  5653  foeq3  5654  f1oeq1  5668  f1oeq2  5669  f1oeq3  5670  fun11iun  5698  mpteqb  5822  rexrnmpt  5882  dffo3  5887  fmptco  5904  dff13  6007  f1imaeq  6014  f1imapss  6015  cbvexfo  6026  f1eqcocnv  6031  fliftcnv  6036  isoeq1  6042  isoeq2  6043  isoeq3  6044  isoeq4  6045  isoeq5  6046  isomin  6060  isowe  6072  fnotovb  6120  mpt2eq123  6136  rexrnmpt2  6188  ottpos  6492  dmtpos  6494  opiota  6538  riotaeqdv  6553  onoviun  6608  smoeq  6615  smoiso2  6634  tfr2b  6660  oarec  6808  oeeui  6848  nnacan  6874  nnmcan  6880  ereq1  6915  ereq2  6916  elecg  6946  ereldm  6951  ixpiin  7091  boxriin  7107  boxcutc  7108  omxpenlem  7212  nnsdomo  7304  enfi  7328  isfinite2  7368  ixpfi2  7408  elfi2  7422  fipwss  7437  ennum  7839  cardsdom2  7880  aleph11  7970  alephiso  7984  fin23lem26  8210  compssiso  8259  isf34lem4  8262  isfin5-2  8276  fin1a2lem5  8289  brdom7disj  8414  brdom6disj  8415  fpwwe2lem8  8517  fpwwe2lem12  8521  fpwwe2lem13  8522  genpass  8891  ltasr  8980  axpre-lttri  9045  infm3  9972  creur  9999  eqreznegel  10566  rpneg  10646  ltxr  10720  icoshftf1o  11025  elfzm11  11121  nn0ennn  11323  nnesq  11508  hashbclem  11706  hashf1lem1  11709  leiso  11713  fz1isolem  11715  rexfiuz  12156  cau4  12165  ello1mpt2  12321  o1lo1  12336  fsumcom2  12563  incexc2  12623  bitsmod  12953  bitscmp  12955  smueqlem  13007  hashdvds  13169  prmreclem2  13290  vdwapun  13347  vdwmc2  13352  imasaddfnlem  13758  comfeq  13937  oppcsect  14004  funcres2b  14099  funcpropd  14102  fullpropd  14122  fthpropd  14123  fthres2b  14132  fthres2c  14133  fullres2c  14141  ffthres2c  14142  fucsect  14174  fucinv  14175  setcsect  14249  tosso  14470  pospropd  14566  odulatb  14575  oduclatb  14576  isipodrs  14592  odudlatb  14627  mndpropd  14726  mhmpropd  14749  issubm2  14754  grppropd  14828  grpinvcnv  14864  conjghm  15041  conjnmzb  15045  ghmpropd  15048  gapm  15088  cmnpropd  15426  ablpropd  15427  eqgabl  15459  gsumcom2  15554  dmdprd  15564  dprdw  15573  subgdmdprd  15597  pgpfac1lem2  15638  pgpfac1lem4  15641  rngpropd  15700  crngpropd  15701  crngunit  15772  unitpropd  15807  isnirred  15810  drngpropd  15867  fldpropd  15868  subrgpropd  15907  rhmpropd  15908  abvpropd  15935  lmodprop2d  16011  lsspropd  16098  lmhmpropd  16150  lbspropd  16176  lvecprop2d  16243  lvecpropd  16244  rrgsupp  16356  opprdomn  16366  fiidomfld  16373  assapropd  16391  psrbagconf1o  16444  mplmonmul  16532  phlpropd  16891  eltopspOLD  16988  istps2OLD  16991  tpspropd  17010  tgss2  17057  lmbr2  17328  ist1-2  17416  ist1-3  17418  subislly  17549  iskgen3  17586  txcnmpt  17661  hausdiag  17682  hauseqlcld  17683  xkococnlem  17696  tgqtop  17749  txhmeo  17840  uffix2  17961  ufildr  17968  txflf  18043  tgphaus  18151  divstgplem  18155  divstgphaus  18157  xpsdsval  18416  blin  18456  blres  18466  xmeterval  18467  xmspropd  18508  mspropd  18509  setsms  18515  metequiv  18544  metustsymOLD  18596  metustsym  18597  restmetu  18622  ngppropd  18683  xrtgioo  18842  metdsge  18884  icopnfcnv  18972  iccpnfcnv  18974  lmhmclm  19116  lmmbr  19216  equivcmet  19273  cmspropd  19307  iunmbl2  19456  ioombl1lem4  19460  mbfaddlem  19555  i1fmullem  19589  itg1mulc  19599  iblcnlem1  19682  iblrelem  19685  iblre  19688  iblcn  19693  limcun  19787  mvth  19881  ofmulrt  20204  resinf1o  20443  quad2  20684  1cubr  20687  dcubic  20691  wilthlem2  20857  dvdsflip  20972  dvdsflf1o  20977  dvdsflsumcom  20978  fsumvma  21002  vmasum  21005  logfac2  21006  logfaclbnd  21011  dchrelbas3  21027  lgsquadlem1  21143  lgsquadlem2  21144  eupath2lem2  21705  isass  21909  ocin  22803  chpsscon3  23010  chscllem2  23145  adjval  23398  pjimai  23684  mdsldmd1i  23839  elat2  23848  mdsymi  23919  rmoxfrdOLD  23984  rmoxfrd  23985  disjrdx  24036  fmptcof2  24081  funcnv5mpt  24089  1stpreima  24100  2ndpreima  24101  zhmnrg  24356  qqhval2  24371  dfrtrclrec2  25148  fprodcom2  25313  dfpo2  25383  dfres3  25387  sscoid  25763  dfrdg4  25800  altopthbg  25818  ax5seg  25882  broutsideof3  26065  ftc1anclem5  26298  istotbnd3  26494  sstotbnd  26498  heibor  26544  isidlc  26639  smprngopr  26676  mrefg2  26775  jm2.23  27081  wepwsolem  27130  dnwech  27137  islssfg2  27160  gicabl  27254  islindf4  27299  pmtrfrn  27391  acsfn1p  27498  isdomn3  27514  ralbidar  27638  rexbidar  27639  sbcrel  27971  sbcfun  27977  dfateq12d  27983  aov0nbovbi  28049  fnotaovb  28052  rexxfrd2  28088  sbcfn  28090  sbcf  28091  elfzomelpfzo  28152  el2wlkonotot1  28406  2pthwlkonot  28417  usg2spot2nb  28528  bnj919  29210  bnj956  29221  bnj976  29222  bnj1366  29275  bnj916  29378  drex1NEW7  29568  drnf1NEW7  29569  drnf2wAUX7  29572  drnf2w2AUX7  29575  drnf2w3AUX7  29578  drsb1NEW7  29580  drnf2OLD7  29790  cbvexdOLD7  29809  sbal2OLD7  29842  islshpsm  29852  lcvexchlem1  29906  opcon1b  30070  isat3  30179  glbconN  30248  cdleme32fva  31308  cdlemg2cex  31462  dibelval3  32019  dib1dim  32037  doch11  32245  dochsordN  32246  mapdordlem1a  32506  mapd11  32511  mapdsord  32527  mapdcnv11N  32531  mapd0  32537
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 179
  Copyright terms: Public domain W3C validator