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  1252  3anbi123d  1253  nanbi1  1300  nanbi2  1301  xorbi12d  1320  hadbi123d  1387  cadbi123d  1388  cad1  1403  had0  1408  nfbidf  1780  drex1  1980  drnf1  1982  drnf2  1983  cbvexd  2022  drsb1  2035  sbal2  2147  eujustALT  2220  eubid  2224  mobid  2251  eqeq1  2372  eqeq2  2375  eleq1  2426  eleq2  2427  nfceqdf  2501  drnfc1  2518  drnfc2  2519  neeq1  2537  neeq2  2538  neleq1  2622  neleq2  2623  ralbida  2642  rexbida  2643  ralbidv2  2650  rexbidv2  2651  r19.21t  2713  r19.23t  2742  ralcom2  2789  reubida  2807  rmobida  2812  raleqf  2817  rexeqf  2818  reueq1f  2819  rmoeq1f  2820  cbvraldva2  2853  cbvrexdva2  2854  dfsbcq  3079  sbcbid  3130  sbcrext  3150  sbcabel  3154  sbnfc2  3227  psseq1  3350  psseq2  3351  ssconb  3396  uneq1  3410  ineq1  3451  difin2  3518  reuun2  3539  reldisj  3586  undif4  3599  disjssun  3600  pssdifcom1  3628  pssdifcom2  3629  sbcss  3653  eltpg  3766  raltpg  3774  rextpg  3775  intmin4  3993  dfiun2g  4037  iindif2  4073  iinin2  4074  disjprg  4121  disjxun  4123  breq  4127  breq1  4128  breq2  4129  treq  4221  opthg2  4350  oteqex2  4361  oteqex  4362  poeq1  4420  soeq1  4436  freq1  4466  weeq1  4484  weeq2  4485  ordeq  4502  limeq  4507  ordunisssuc  4598  reusv2lem5  4642  reusv5OLD  4647  reusv7OLD  4649  rexxfrd  4652  rexxfr2d  4654  rabxfrd  4658  iunpw  4673  tfinds  4753  opthprc  4839  wesn  4864  releq  4874  eqrel  4880  eqrelrel  4891  xpiindi  4924  brcnvg  4965  brresg  5066  resieq  5068  dmsnopg  5247  dfco2a  5276  iotaeq  5330  sniota  5349  imadif  5432  fneq1  5438  fneq2  5439  feq1  5480  feq2  5481  feq3  5482  f1eq1  5538  f1eq2  5539  f1eq3  5540  foeq1  5553  foeq2  5554  foeq3  5555  f1oeq1  5569  f1oeq2  5570  f1oeq3  5571  fun11iun  5599  mpteqb  5721  rexrnmpt  5781  dffo3  5786  fmptco  5802  dff13  5904  f1imaeq  5911  f1imapss  5912  cbvexfo  5923  f1eqcocnv  5928  fliftcnv  5933  isoeq1  5939  isoeq2  5940  isoeq3  5941  isoeq4  5942  isoeq5  5943  isomin  5957  isowe  5969  fnotovb  6017  mpt2eq123  6033  rexrnmpt2  6085  ottpos  6386  dmtpos  6388  opiota  6432  riotaeqdv  6447  onoviun  6502  smoeq  6509  smoiso2  6528  tfr2b  6554  oarec  6702  oeeui  6742  nnacan  6768  nnmcan  6774  ereq1  6809  ereq2  6810  elecg  6840  ereldm  6845  ixpiin  6985  boxriin  7001  boxcutc  7002  omxpenlem  7106  nnsdomo  7198  enfi  7222  isfinite2  7262  ixpfi2  7301  elfi2  7315  fipwss  7329  ennum  7727  cardsdom2  7768  aleph11  7858  alephiso  7872  fin23lem26  8098  compssiso  8147  isf34lem4  8150  isfin5-2  8164  fin1a2lem5  8177  brdom7disj  8303  brdom6disj  8304  fpwwe2lem8  8406  fpwwe2lem12  8410  fpwwe2lem13  8411  genpass  8780  ltasr  8869  axpre-lttri  8934  infm3  9860  creur  9887  eqreznegel  10454  rpneg  10534  ltxr  10608  icoshftf1o  10912  elfzm11  11006  nn0ennn  11205  nnesq  11390  hashbclem  11588  hashf1lem1  11591  leiso  11595  fz1isolem  11597  rexfiuz  12038  cau4  12047  ello1mpt2  12203  o1lo1  12218  fsumcom2  12445  incexc2  12505  bitsmod  12835  bitscmp  12837  smueqlem  12889  hashdvds  13051  prmreclem2  13172  vdwapun  13229  vdwmc2  13234  imasaddfnlem  13640  comfeq  13819  oppcsect  13886  funcres2b  13981  funcpropd  13984  fullpropd  14004  fthpropd  14005  fthres2b  14014  fthres2c  14015  fullres2c  14023  ffthres2c  14024  fucsect  14056  fucinv  14057  setcsect  14131  tosso  14352  pospropd  14448  odulatb  14457  oduclatb  14458  isipodrs  14474  odudlatb  14509  mndpropd  14608  mhmpropd  14631  issubm2  14636  grppropd  14710  grpinvcnv  14746  conjghm  14923  conjnmzb  14927  ghmpropd  14930  gapm  14970  cmnpropd  15308  ablpropd  15309  eqgabl  15341  gsumcom2  15436  dmdprd  15446  dprdw  15455  subgdmdprd  15479  pgpfac1lem2  15520  pgpfac1lem4  15523  rngpropd  15582  crngpropd  15583  crngunit  15654  unitpropd  15689  isnirred  15692  drngpropd  15749  fldpropd  15750  subrgpropd  15789  rhmpropd  15790  abvpropd  15817  lmodprop2d  15897  lsspropd  15984  lmhmpropd  16036  lbspropd  16062  lvecprop2d  16129  lvecpropd  16130  rrgsupp  16242  opprdomn  16252  fiidomfld  16259  assapropd  16277  psrbagconf1o  16330  mplmonmul  16418  phlpropd  16776  eltopspOLD  16873  istps2OLD  16876  tpspropd  16895  tgss2  16942  lmbr2  17206  ist1-2  17292  ist1-3  17294  subislly  17424  iskgen3  17461  txcnmpt  17535  hausdiag  17556  hauseqlcld  17557  xkococnlem  17570  tgqtop  17620  txhmeo  17711  uffix2  17832  ufildr  17839  txflf  17914  tgphaus  18012  divstgplem  18016  divstgphaus  18018  xpsdsval  18158  blin  18183  blres  18190  xmeterval  18191  xmspropd  18232  mspropd  18233  setsms  18239  metequiv  18268  ngppropd  18366  xrtgioo  18525  metdsge  18567  icopnfcnv  18655  iccpnfcnv  18657  lmhmclm  18799  lmmbr  18899  equivcmet  18956  cmspropd  18986  iunmbl2  19129  ioombl1lem4  19133  mbfaddlem  19230  i1fmullem  19264  itg1mulc  19274  iblcnlem1  19357  iblrelem  19360  iblre  19363  iblcn  19368  limcun  19460  mvth  19554  ofmulrt  19877  resinf1o  20116  quad2  20357  1cubr  20360  dcubic  20364  wilthlem2  20530  dvdsflip  20645  dvdsflf1o  20650  dvdsflsumcom  20651  fsumvma  20675  vmasum  20678  logfac2  20679  logfaclbnd  20684  dchrelbas3  20700  lgsquadlem1  20816  lgsquadlem2  20817  isass  21294  ocin  22188  chpsscon3  22395  chscllem2  22530  adjval  22783  pjimai  23069  mdsldmd1i  23224  elat2  23233  mdsymi  23304  rmoxfrdOLD  23373  rmoxfrd  23374  disjrdx  23428  fmptcof2  23479  1stpreima  23498  2ndpreima  23499  metustsym  23798  restmetu  23814  zhmnrg  23825  qqhval2  23838  eupath2lem2  24489  dfrtrclrec2  24627  dfpo2  24853  dfres3  24857  dfrdg4  25230  altopthbg  25244  ax5seg  25308  broutsideof3  25491  nabi1  25570  nabi2  25571  istotbnd3  26001  sstotbnd  26005  heibor  26051  isidlc  26146  smprngopr  26183  mrefg2  26288  jm2.23  26595  wepwsolem  26644  dnwech  26651  islssfg2  26675  gicabl  26769  islindf4  26814  pmtrfrn  26906  acsfn1p  27013  isdomn3  27029  ralbidar  27154  rexbidar  27155  sbcrel  27487  sbcfun  27493  dfateq12d  27500  aov0nbovbi  27566  fnotaovb  27569  bnj919  28561  bnj956  28572  bnj976  28573  bnj1366  28626  bnj916  28729  drex1NEW7  28919  drnf1NEW7  28920  drnf2wAUX7  28923  drnf2w2AUX7  28926  drnf2w3AUX7  28929  drsb1NEW7  28931  drnf2OLD7  29119  cbvexdOLD7  29138  sbal2OLD7  29173  islshpsm  29241  lcvexchlem1  29295  opcon1b  29459  isat3  29568  glbconN  29637  cdleme32fva  30697  cdlemg2cex  30851  dibelval3  31408  dib1dim  31426  doch11  31634  dochsordN  31635  mapdordlem1a  31895  mapd11  31900  mapdsord  31916  mapdcnv11N  31920  mapd0  31926
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