Theorem 3bitr4g 291

Description: More general version of 3bitr4i 280. Useful for converting definitions in a formula. (Contributed by NM, 11-May-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

Step	Hyp	Ref	Expression
1		3bitr4g.2	. . 3 |- ( th <-> ps )
2		3bitr4g.1	. . 3 |- ( ph -> ( ps <-> ch ) )
3	1, 2	syl5bb 260	. 2 |- ( ph -> ( th <-> ch ) )
4		3bitr4g.3	. 2 |- ( ta <-> ch )
5	3, 4	syl6bbr 266	1 |- ( ph -> ( th <-> ta ) )

Syntax hints:   -> wi 4   <-> wb 187

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 188

This theorem is referenced by:  bibi1d  320  pm5.32rd  644  orbi2d  706  orbi1d  707  3orbi123d  1334  3anbi123d  1335  nanbi1  1391  nanbi2  1392  xorbi12d  1417  hadbi123d  1491  had0  1500  cadbi123d  1506  nfbidf  1942  19.23t  1968  cbvexd  2086  drex1  2130  drnf1  2132  drsb1  2177  eujustALT  2274  eubid  2289  mobid  2290  eqeq1d  2425  eqeq1dALT  2426  eqeq2d  2433  eleq1d  2485  eleq2d  2486  eleq2dOLD  2487  eleq2dALT  2488  nfceqdf  2560  drnfc1  2581  drnfc2  2582  neleq12d  2700  r19.21t  2757  r19.21tOLD  2758  ralbida  2793  ralbidv2  2795  r19.23t  2837  rexbida  2868  rexbidv2  2869  ralcom2  2927  reubida  2945  rmobida  2950  raleqf  2955  rexeqf  2956  reueq1f  2957  rmoeq1f  2958  cbvraldva2  2995  cbvrexdva2  2996  dfsbcq  3239  sbceqbid  3244  sbcbi2  3286  sbcbid  3291  sbcrext  3311  sbcabel  3315  psseq1  3490  psseq2  3491  ssconb  3536  uneq1  3551  ineq1  3595  difin2  3673  reuun2  3694  sbcnel12g  3742  sbnfc2  3764  reldisj  3776  undif4  3789  disjssun  3790  pssdifcom1  3821  pssdifcom2  3822  sbcssg  3848  eltpg  3980  raltpg  3989  rextpg  3990  r19.12sn  4003  intmin4  4223  dfiun2g  4269  iindif2  4306  iinin2  4307  disjprg  4357  disjxun  4359  breq  4363  breq1  4364  breq2  4365  treq  4462  reusv2lem5  4567  rexxfrd  4574  rexxfr2d  4576  rabxfrd  4580  opthg2  4636  oteqex2  4650  oteqex  4651  poeq1  4715  soeq1  4731  freq1  4761  weeq1  4779  weeq2  4780  opthprc  4839  wesn  4863  releq  4874  sbcrel  4878  eqrel  4881  eqrelrel  4893  xpiindi  4927  brcnvg  4972  brresg  5070  resieq  5072  dmsnopg  5264  dfco2a  5292  ordeq  5387  limeq  5392  ordunisssuc  5482  iotaeq  5511  sniota  5530  sbcfung  5562  imadif  5614  fneq1  5620  fneq2  5621  feq1  5666  feq2  5667  feq3  5668  sbcfng  5681  sbcfg  5682  f1eq1  5729  f1eq2  5730  f1eq3  5731  foeq1  5744  foeq2  5745  foeq3  5746  f1oeq1  5760  f1oeq2  5761  f1oeq3  5762  mpteqb  5919  rexrnmpt  5986  dffo3  5991  fmptco  6010  dff13  6113  f1imaeq  6120  f1imapss  6121  cbvexfo  6142  f1eqcocnv  6153  fliftcnv  6158  isoeq1  6164  isoeq2  6165  isoeq3  6166  isoeq4  6167  isoeq5  6168  isomin  6182  isowe  6194  fnotovb  6285  mpt2eq123  6303  rexrnmpt2  6365  iunpw  6558  tfinds  6639  fun11iun  6706  opiota  6805  ottpos  6933  dmtpos  6935  onoviun  7012  smoeq  7019  smoiso2  7038  tfr2b  7064  oarec  7213  oeeui  7253  nnacan  7279  nnmcan  7285  ereq1  7320  ereq2  7321  elecg  7352  ereldm  7357  ixpiin  7498  boxriin  7514  boxcutc  7515  omxpenlem  7621  nnsdomo  7715  enfi  7736  isfinite2  7777  ixpfi2  7820  elfi2  7876  fipwss  7891  ennum  8328  cardsdom2  8369  aleph11  8461  alephiso  8475  fin23lem26  8701  compssiso  8750  isf34lem4  8753  isfin5-2  8767  fin1a2lem5  8780  brdom7disj  8905  brdom6disj  8906  fpwwe2lem8  9008  fpwwe2lem12  9012  fpwwe2lem13  9013  genpass  9380  ltasr  9470  axpre-lttri  9535  infm3  10514  creur  10549  eqreznegel  11195  rpneg  11278  ltxr  11361  icoshftf1o  11701  elfzm11  11811  elfzomelpfzo  11958  nn0ennn  12137  nnesq  12341  hashbclem  12558  hashf1lem1  12561  leiso  12565  fz1isolem  12567  pr2pwpr  12579  repsdf2  12822  dfrtrclrec2  13059  rexfiuz  13349  cau4  13358  ello1mpt2  13524  o1lo1  13539  fsumcom2  13773  incexc2  13834  fprodcom2  13976  bitsmod  14348  bitscmp  14350  smueqlem  14402  ncoprmgcdne1b  14593  hashdvds  14661  prmreclem2  14799  vdwapun  14862  vdwmc2  14867  imasaddfnlem  15372  comfeq  15549  oppcsect  15621  funcres2b  15740  funcpropd  15743  fullpropd  15763  fthpropd  15764  fthres2b  15773  fthres2c  15774  fullres2c  15782  ffthres2c  15783  fucsect  15815  fucinv  15816  setcsect  15922  tosso  16220  pospropd  16318  odulatb  16327  oduclatb  16328  isipodrs  16345  odudlatb  16380  issgrpv  16467  issgrpn0  16468  mndpropd  16500  mhmpropd  16526  issubm2  16533  grppropd  16622  grpinvcnv  16660  conjghm  16851  conjnmzb  16855  ghmpropd  16858  gapm  16898  symg1bas  16975  pmtrfrn  17037  cmnpropd  17377  ablpropd  17378  eqgabl  17413  gsumcom2  17545  dmdprd  17568  dprdw  17580  subgdmdprd  17605  pgpfac1lem2  17646  pgpfac1lem4  17649  ringpropd  17750  crngpropd  17751  crngunit  17828  unitpropd  17863  isnirred  17866  drngpropd  17940  fldpropd  17941  subrgpropd  17980  rhmpropd  17981  abvpropd  18008  lmodprop2d  18088  lsspropd  18178  lmhmpropd  18234  lbspropd  18260  lvecprop2d  18327  lvecpropd  18328  opprdomn  18463  fiidomfld  18470  assapropd  18489  psrbagconf1o  18536  mplmonmul  18626  phlpropd  19159  mat1dimbas  19434  tpspropd  19892  tgss2  19940  lmbr2  20212  ist1-2  20300  ist1-3  20302  subislly  20433  dissnlocfin  20481  iskgen3  20501  txcnmpt  20576  hausdiag  20597  hauseqlcld  20598  xkococnlem  20611  tgqtop  20664  txhmeo  20755  uffix2  20876  ufildr  20883  txflf  20958  tgphaus  21068  qustgplem  21072  qustgphaus  21074  xpsdsval  21333  blin  21373  blres  21383  xmeterval  21384  xmspropd  21425  mspropd  21426  setsms  21432  metequiv  21461  metustsym  21507  restmetu  21522  ngppropd  21582  xrtgioo  21761  metdsge  21803  metdsgeOLD  21818  icopnfcnv  21907  iccpnfcnv  21909  lmhmclm  22054  lmmbr  22165  equivcmet  22222  cmspropd  22254  iunmbl2  22447  ioombl1lem4  22451  mbfaddlem  22553  i1fmullem  22589  itg1mulc  22599  iblcnlem1  22682  iblrelem  22685  iblre  22688  iblcn  22693  limcun  22787  mvth  22881  ofmulrt  23172  resinf1o  23422  quad2  23702  1cubr  23705  dcubic  23709  wilthlem2  23931  dvdsflip  24048  dvdsflf1o  24053  dvdsflsumcom  24054  fsumvma  24078  vmasum  24081  logfac2  24082  logfaclbnd  24087  dchrelbas3  24103  lgsquadlem1  24219  lgsquadlem2  24220  ax5seg  24905  clwwlknscsh  25484  el2wlkonotot1  25539  2pthwlkonot  25550  rusgranumwlkb0  25618  eupath2lem2  25643  usg2spot2nb  25730  numclwwlkovfel2  25748  isass  25981  ocin  26886  chpsscon3  27093  chscllem2  27228  adjval  27480  pjimai  27766  mdsldmd1i  27921  elat2  27930  mdsymi  28001  sbceqbidf  28054  rmoxfrdOLD  28065  rmoxfrd  28066  disjrdx  28142  eqrelrd2  28163  fmptcof2  28200  ofpreima  28209  funcnv5mpt  28213  1stpreima  28228  2ndpreima  28229  fpwrelmapffslem  28262  smatrcl  28569  locfinreflem  28614  zhmnrg  28718  qqhval2  28733  ismntop  28777  bnj919  29525  bnj956  29535  bnj976  29536  bnj1366  29588  bnj916  29691  dfpo2  30341  dfres3  30345  sscoid  30624  dfrdg4  30662  altopthbg  30679  broutsideof3  30837  bj-nfbi  31156  bj-cbvexdv  31242  bj-drex1v  31267  bj-drnf1v  31268  bj-eleq1w  31366  bj-eleq2w  31367  bj-ax8  31406  wl-nanbi1  31762  wl-nanbi2  31763  wl-sb8eut  31813  wl-sb8mot  31814  poimirlem17  31864  poimirlem19  31866  poimirlem20  31867  poimirlem25  31872  ftc1anclem5  31928  istotbnd3  32010  sstotbnd  32014  heibor  32060  isidlc  32155  smprngopr  32192  islshpsm  32458  lcvexchlem1  32512  opcon1b  32676  isat3  32785  glbconN  32854  cdleme32fva  33916  cdlemg2cex  34070  dibelval3  34627  dib1dim  34645  doch11  34853  dochsordN  34854  mapdordlem1a  35114  mapd11  35119  mapdsord  35135  mapdcnv11N  35139  mapd0  35145  mrefg2  35461  jm2.23  35764  wepwsolem  35813  dnwech  35819  islssfg2  35842  gicabl  35870  acsfn1p  35978  isdomn3  35994  ifpbi2  36023  ifpbi3  36024  ifpbi23  36029  ifpbi1  36034  ifpbi12  36045  ifpbi13  36046  ifpbi123  36047  pwinfig  36078  inintabd  36098  cnvcnvintabd  36119  cnvintabd  36122  intimag  36161  briunov2  36187  heeq12  36284  sbcheg  36287  ralbidar  36711  rexbidar  36712  trsbc  36814  dffo3f  37354  iccintsng  37516  dfateq12d  38444  aov0nbovbi  38510  fnotaovb  38513  rexxfrd2  38816  usgredgedga  39054  nbumgrvtx  39150  mgmhmpropd  39376  rngcsect  39573  rngcsectALTV  39585  ringcsect  39624  ringcsectALTV  39648  lindslinindsimp2lem5  39848