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  1251  3anbi123d  1252  xorbi12d  1306  hadbi123d  1372  cadbi123d  1373  cad1  1388  had0  1393  nfbidf  1756  drex1  1909  drnf1  1911  drnf2  1912  cbvexd  1951  drsb1  1964  sbal2  2075  eujustALT  2148  eubid  2152  mobid  2179  eqeq1  2291  eqeq2  2294  eleq1  2345  eleq2  2346  nfceqdf  2420  drnfc1  2437  drnfc2  2438  neeq1  2456  neeq2  2457  neleq1  2539  neleq2  2540  ralbida  2559  rexbida  2560  ralbidv2  2567  rexbidv2  2568  r19.21t  2630  r19.23t  2659  ralcom2  2706  reubida  2724  rmobida  2729  raleqf  2734  rexeqf  2735  reueq1f  2736  rmoeq1f  2737  cbvraldva2  2770  cbvrexdva2  2771  dfsbcq  2995  sbcbid  3046  sbcrext  3066  sbcabel  3070  sbnfc2  3143  psseq1  3265  psseq2  3266  ssconb  3311  uneq1  3324  ineq1  3365  difin2  3432  reuun2  3453  reldisj  3500  undif4  3513  disjssun  3514  pssdifcom1  3541  pssdifcom2  3542  sbcss  3566  eltpg  3678  raltpg  3686  rextpg  3687  intmin4  3893  dfiun2g  3937  iindif2  3973  iinin2  3974  disjprg  4021  disjxun  4023  breq  4027  breq1  4028  breq2  4029  treq  4121  opthg2  4249  oteqex2  4260  oteqex  4261  poeq1  4319  soeq1  4335  freq1  4365  weeq1  4383  weeq2  4384  ordeq  4401  limeq  4406  ordunisssuc  4497  reusv2lem5  4541  reusv5OLD  4546  reusv7OLD  4548  rexxfrd  4551  rexxfr2d  4553  rabxfrd  4557  iunpw  4572  tfinds  4652  opthprc  4738  wesn  4763  releq  4773  eqrel  4779  eqrelrel  4790  xpiindi  4823  brcnvg  4864  brresg  4965  resieq  4967  dmsnopg  5146  dfco2a  5175  iotaeq  5229  sniota  5248  imadif  5329  fneq1  5335  fneq2  5336  feq1  5377  feq2  5378  feq3  5379  f1eq1  5434  f1eq2  5435  f1eq3  5436  foeq1  5449  foeq2  5450  foeq3  5451  f1oeq1  5465  f1oeq2  5466  f1oeq3  5467  fun11iun  5495  mpteqb  5616  rexrnmpt  5672  dffo3  5677  fmptco  5693  dff13  5785  f1imaeq  5791  f1imapss  5792  cbvexfo  5802  f1eqcocnv  5807  fliftcnv  5812  isoeq1  5818  isoeq2  5819  isoeq3  5820  isoeq4  5821  isoeq5  5822  isomin  5836  isowe  5848  fnotovb  5896  mpt2eq123  5909  rexrnmpt2  5961  ottpos  6246  dmtpos  6248  opiota  6292  riotaeqdv  6307  onoviun  6362  smoeq  6369  smoiso2  6388  tfr2b  6414  oarec  6562  oeeui  6602  nnacan  6628  nnmcan  6634  ereq1  6669  ereq2  6670  elecg  6700  ereldm  6705  ixpiin  6844  boxriin  6860  boxcutc  6861  omxpenlem  6965  nnsdomo  7057  enfi  7081  isfinite2  7117  ixpfi2  7156  elfi2  7170  fipwss  7184  ennum  7582  cardsdom2  7623  aleph11  7713  alephiso  7727  fin23lem26  7953  compssiso  8002  isf34lem4  8005  isfin5-2  8019  fin1a2lem5  8032  brdom7disj  8158  brdom6disj  8159  fpwwe2lem8  8261  fpwwe2lem12  8265  fpwwe2lem13  8266  genpass  8635  ltasr  8724  axpre-lttri  8789  infm3  9715  creur  9742  eqreznegel  10305  rpneg  10385  ltxr  10459  icoshftf1o  10761  elfzm11  10855  nn0ennn  11043  nnesq  11227  hashbclem  11392  hashf1lem1  11395  leiso  11399  fz1isolem  11401  rexfiuz  11833  cau4  11842  ello1mpt2  11998  o1lo1  12013  fsumcom2  12239  incexc2  12299  bitsmod  12629  bitscmp  12631  smueqlem  12683  hashdvds  12845  prmreclem2  12966  vdwapun  13023  vdwmc2  13028  imasaddfnlem  13432  comfeq  13611  oppcsect  13678  funcres2b  13773  funcpropd  13776  fullpropd  13796  fthpropd  13797  fthres2b  13806  fthres2c  13807  fullres2c  13815  ffthres2c  13816  fucsect  13848  fucinv  13849  setcsect  13923  tosso  14144  pospropd  14240  odulatb  14249  oduclatb  14250  isipodrs  14266  odudlatb  14301  mndpropd  14400  mhmpropd  14423  issubm2  14428  grppropd  14502  grpinvcnv  14538  conjghm  14715  conjnmzb  14719  ghmpropd  14722  gapm  14762  cmnpropd  15100  ablpropd  15101  eqgabl  15133  gsumcom2  15228  dmdprd  15238  dprdw  15247  subgdmdprd  15271  pgpfac1lem2  15312  pgpfac1lem4  15315  rngpropd  15374  crngpropd  15375  crngunit  15446  unitpropd  15481  isnirred  15484  drngpropd  15541  fldpropd  15542  subrgpropd  15581  rhmpropd  15582  abvpropd  15609  lmodprop2d  15689  lsspropd  15776  lmhmpropd  15828  lbspropd  15854  lvecprop2d  15921  lvecpropd  15922  rrgsupp  16034  opprdomn  16044  fiidomfld  16051  assapropd  16069  psrbagconf1o  16122  mplmonmul  16210  phlpropd  16561  eltopspOLD  16658  istps2OLD  16661  tpspropd  16680  tgss2  16727  lmbr2  16991  ist1-2  17077  ist1-3  17079  subislly  17209  iskgen3  17246  txcnmpt  17320  hausdiag  17341  hauseqlcld  17342  xkococnlem  17355  tgqtop  17405  txhmeo  17496  uffix2  17621  ufildr  17628  txflf  17703  tgphaus  17801  divstgplem  17805  divstgphaus  17807  xpsdsval  17947  blin  17972  blres  17979  xmeterval  17980  xmspropd  18021  mspropd  18022  setsms  18028  metequiv  18057  ngppropd  18155  xrtgioo  18314  metdsge  18355  icopnfcnv  18442  iccpnfcnv  18444  lmhmclm  18586  lmmbr  18686  equivcmet  18743  cmspropd  18773  iunmbl2  18916  ioombl1lem4  18920  mbfaddlem  19017  i1fmullem  19051  itg1mulc  19061  iblcnlem1  19144  iblrelem  19147  iblre  19150  iblcn  19155  limcun  19247  mvth  19341  ofmulrt  19664  resinf1o  19900  quad2  20137  1cubr  20140  dcubic  20144  wilthlem2  20309  dvdsflip  20424  dvdsflf1o  20429  dvdsflsumcom  20430  fsumvma  20454  vmasum  20457  logfac2  20458  logfaclbnd  20463  dchrelbas3  20479  lgsquadlem1  20595  lgsquadlem2  20596  isass  20985  ocin  21877  chpsscon3  22084  chscllem2  22219  adjval  22472  pjimai  22758  mdsldmd1i  22913  elat2  22922  mdsymi  22993  rmoxfrdOLD  23148  rmoxfrd  23149  fmptcof2  23231  disjrdx  23372  eupath2lem2  23904  dfrtrclrec2  24042  dfpo2  24114  dfres3  24118  dfrdg4  24490  altopthbg  24504  ax5seg  24568  broutsideof3  24751  nabi1  24830  nabi2  24831  relrefcnv  25128  iscst4  25188  trinv  25406  svs3  25499  cnvtr  25627  dualded  25794  vtarsuelt  25906  istotbnd3  26506  sstotbnd  26510  heibor  26556  isidlc  26651  smprngopr  26688  mrefg2  26793  jm2.23  27100  wepwsolem  27149  dnwech  27156  islssfg2  27180  gicabl  27274  islindf4  27319  pmtrfrn  27411  acsfn1p  27518  isdomn3  27534  ralbidar  27659  rexbidar  27660  sbcrel  27990  sbcfun  27996  dfateq12d  28003  aov0nbovbi  28066  fnotaovb  28069  bnj919  28870  bnj956  28881  bnj976  28882  bnj1366  28935  bnj916  29038  islshpsm  29243  lcvexchlem1  29297  opcon1b  29461  isat3  29570  glbconN  29639  cdleme32fva  30699  cdlemg2cex  30853  dibelval3  31410  dib1dim  31428  doch11  31636  dochsordN  31637  mapdordlem1a  31897  mapd11  31902  mapdsord  31918  mapdcnv11N  31922  mapd0  31928
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