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  1493  had0  1502  cadbi123d  1508  nfbidf  1940  19.23t  1966  cbvexd  2082  drex1  2125  drnf1  2127  drsb1  2172  eujustALT  2269  eubid  2286  mobid  2287  eqeq1d  2431  eqeq1dALT  2432  eqeq1OLD  2434  eqeq2d  2443  eqeq2OLD  2445  eleq1d  2498  eleq2d  2499  eleq2dALT  2500  eleq1OLD  2503  eleq2OLD  2504  nfceqdf  2586  drnfc1  2610  drnfc2  2611  neeq1OLD  2713  neeq2OLD  2715  neleq12d  2769  neleq1OLD  2771  neleq2OLD  2773  r19.21t  2829  r19.21tOLD  2830  ralbida  2865  ralbidv2  2867  r19.23t  2910  rexbida  2941  rexbidv2  2942  ralcom2  3000  reubida  3018  rmobida  3023  raleqf  3028  rexeqf  3029  reueq1f  3030  rmoeq1f  3031  cbvraldva2  3066  cbvrexdva2  3067  dfsbcq  3307  sbceqbid  3312  sbcbi2  3354  sbcbid  3359  sbcrext  3379  sbcabel  3383  psseq1  3558  psseq2  3559  ssconb  3604  uneq1  3619  ineq1  3663  difin2  3741  reuun2  3762  sbcnel12g  3808  sbnfc2  3830  reldisj  3842  undif4  3855  disjssun  3856  pssdifcom1  3887  pssdifcom2  3888  sbcssg  3914  eltpg  4045  raltpg  4054  rextpg  4055  r19.12sn  4068  intmin4  4288  dfiun2g  4334  iindif2  4371  iinin2  4372  disjprg  4422  disjxun  4424  breq  4428  breq1  4429  breq2  4430  treq  4526  reusv2lem5  4630  rexxfrd  4637  rexxfr2d  4639  rabxfrd  4643  opthg2  4699  oteqex2  4713  oteqex  4714  poeq1  4778  soeq1  4794  freq1  4824  weeq1  4842  weeq2  4843  opthprc  4902  wesn  4926  releq  4937  sbcrel  4941  eqrel  4944  eqrelrel  4956  xpiindi  4990  brcnvg  5035  brresg  5133  resieq  5135  dmsnopg  5327  dfco2a  5355  ordeq  5449  limeq  5454  ordunisssuc  5544  iotaeq  5573  sniota  5592  sbcfung  5624  imadif  5676  fneq1  5682  fneq2  5683  feq1  5728  feq2  5729  feq3  5730  sbcfng  5743  sbcfg  5744  f1eq1  5791  f1eq2  5792  f1eq3  5793  foeq1  5806  foeq2  5807  foeq3  5808  f1oeq1  5822  f1oeq2  5823  f1oeq3  5824  mpteqb  5980  rexrnmpt  6047  dffo3  6052  fmptco  6071  dff13  6174  f1imaeq  6181  f1imapss  6182  cbvexfo  6203  f1eqcocnv  6214  fliftcnv  6219  isoeq1  6225  isoeq2  6226  isoeq3  6227  isoeq4  6228  isoeq5  6229  isomin  6243  isowe  6255  fnotovb  6346  mpt2eq123  6364  rexrnmpt2  6426  iunpw  6619  tfinds  6700  fun11iun  6767  opiota  6866  ottpos  6991  dmtpos  6993  onoviun  7070  smoeq  7077  smoiso2  7096  tfr2b  7122  oarec  7271  oeeui  7311  nnacan  7337  nnmcan  7343  ereq1  7378  ereq2  7379  elecg  7410  ereldm  7415  ixpiin  7556  boxriin  7572  boxcutc  7573  omxpenlem  7679  nnsdomo  7773  enfi  7794  isfinite2  7835  ixpfi2  7878  elfi2  7934  fipwss  7949  ennum  8380  cardsdom2  8421  aleph11  8513  alephiso  8527  fin23lem26  8753  compssiso  8802  isf34lem4  8805  isfin5-2  8819  fin1a2lem5  8832  brdom7disj  8957  brdom6disj  8958  fpwwe2lem8  9061  fpwwe2lem12  9065  fpwwe2lem13  9066  genpass  9433  ltasr  9523  axpre-lttri  9588  infm3  10568  creur  10603  eqreznegel  11249  rpneg  11332  ltxr  11415  icoshftf1o  11753  elfzm11  11863  elfzomelpfzo  12010  nn0ennn  12189  nnesq  12393  hashbclem  12610  hashf1lem1  12613  leiso  12617  fz1isolem  12619  pr2pwpr  12629  repsdf2  12866  dfrtrclrec2  13099  rexfiuz  13389  cau4  13398  ello1mpt2  13564  o1lo1  13579  fsumcom2  13813  incexc2  13874  fprodcom2  14016  bitsmod  14384  bitscmp  14386  smueqlem  14438  ncoprmgcdne1b  14617  hashdvds  14683  prmreclem2  14815  vdwapun  14878  vdwmc2  14883  imasaddfnlem  15376  comfeq  15553  oppcsect  15625  funcres2b  15744  funcpropd  15747  fullpropd  15767  fthpropd  15768  fthres2b  15777  fthres2c  15778  fullres2c  15786  ffthres2c  15787  fucsect  15819  fucinv  15820  setcsect  15926  tosso  16224  pospropd  16322  odulatb  16331  oduclatb  16332  isipodrs  16349  odudlatb  16384  issgrpv  16471  issgrpn0  16472  mndpropd  16504  mhmpropd  16530  issubm2  16537  grppropd  16626  grpinvcnv  16664  conjghm  16855  conjnmzb  16859  ghmpropd  16862  gapm  16902  symg1bas  16979  pmtrfrn  17041  cmnpropd  17365  ablpropd  17366  eqgabl  17401  gsumcom2  17533  dmdprd  17556  dprdw  17568  subgdmdprd  17593  pgpfac1lem2  17634  pgpfac1lem4  17637  ringpropd  17738  crngpropd  17739  crngunit  17816  unitpropd  17851  isnirred  17854  drngpropd  17928  fldpropd  17929  subrgpropd  17968  rhmpropd  17969  abvpropd  17996  lmodprop2d  18076  lsspropd  18166  lmhmpropd  18222  lbspropd  18248  lvecprop2d  18315  lvecpropd  18316  opprdomn  18451  fiidomfld  18458  assapropd  18477  psrbagconf1o  18524  mplmonmul  18614  phlpropd  19144  mat1dimbas  19419  tpspropd  19877  tgss2  19925  lmbr2  20197  ist1-2  20285  ist1-3  20287  subislly  20418  dissnlocfin  20466  iskgen3  20486  txcnmpt  20561  hausdiag  20582  hauseqlcld  20583  xkococnlem  20596  tgqtop  20649  txhmeo  20740  uffix2  20861  ufildr  20868  txflf  20943  tgphaus  21053  qustgplem  21057  qustgphaus  21059  xpsdsval  21318  blin  21358  blres  21368  xmeterval  21369  xmspropd  21410  mspropd  21411  setsms  21417  metequiv  21446  metustsym  21492  restmetu  21507  ngppropd  21567  xrtgioo  21726  metdsge  21768  icopnfcnv  21857  iccpnfcnv  21859  lmhmclm  22001  lmmbr  22112  equivcmet  22169  cmspropd  22201  iunmbl2  22378  ioombl1lem4  22382  mbfaddlem  22484  i1fmullem  22520  itg1mulc  22530  iblcnlem1  22613  iblrelem  22616  iblre  22619  iblcn  22624  limcun  22718  mvth  22812  ofmulrt  23094  resinf1o  23341  quad2  23621  1cubr  23624  dcubic  23628  wilthlem2  23850  dvdsflip  23965  dvdsflf1o  23970  dvdsflsumcom  23971  fsumvma  23995  vmasum  23998  logfac2  23999  logfaclbnd  24004  dchrelbas3  24020  lgsquadlem1  24136  lgsquadlem2  24137  ax5seg  24805  clwwlknscsh  25383  el2wlkonotot1  25438  2pthwlkonot  25449  rusgranumwlkb0  25517  eupath2lem2  25542  usg2spot2nb  25629  numclwwlkovfel2  25647  isass  25880  ocin  26775  chpsscon3  26982  chscllem2  27117  adjval  27369  pjimai  27655  mdsldmd1i  27810  elat2  27819  mdsymi  27890  sbceqbidf  27943  rmoxfrdOLD  27954  rmoxfrd  27955  disjrdx  28031  eqrelrd2  28052  fmptcof2  28090  ofpreima  28099  funcnv5mpt  28103  1stpreima  28118  2ndpreima  28119  fpwrelmapffslem  28151  smatrcl  28452  locfinreflem  28497  zhmnrg  28601  qqhval2  28616  ismntop  28660  bnj919  29357  bnj956  29367  bnj976  29368  bnj1366  29420  bnj916  29523  dfpo2  30173  dfres3  30177  sscoid  30456  dfrdg4  30494  altopthbg  30511  broutsideof3  30669  bj-nfbi  30987  bj-cbvexdv  31072  bj-drex1v  31098  bj-drnf1v  31099  bj-eleq1w  31197  bj-eleq2w  31198  bj-ax8  31236  wl-nanbi1  31553  wl-nanbi2  31554  wl-sb8eut  31600  wl-sb8mot  31601  poimirlem17  31651  poimirlem19  31653  poimirlem20  31654  poimirlem25  31659  ftc1anclem5  31715  istotbnd3  31797  sstotbnd  31801  heibor  31847  isidlc  31942  smprngopr  31979  islshpsm  32245  lcvexchlem1  32299  opcon1b  32463  isat3  32572  glbconN  32641  cdleme32fva  33703  cdlemg2cex  33857  dibelval3  34414  dib1dim  34432  doch11  34640  dochsordN  34641  mapdordlem1a  34901  mapd11  34906  mapdsord  34922  mapdcnv11N  34926  mapd0  34932  mrefg2  35248  jm2.23  35547  wepwsolem  35596  dnwech  35602  islssfg2  35625  gicabl  35653  acsfn1p  35754  isdomn3  35770  ifpbi2  35799  ifpbi3  35800  ifpbi23  35805  ifpbi1  35810  ifpbi12  35821  ifpbi13  35822  ifpbi123  35823  pwinfig  35854  intimag  35877  briunov2  35903  heeq12  35998  sbcheg  36001  ralbidar  36425  rexbidar  36426  trsbc  36528  dffo3f  37063  iccintsng  37199  dfateq12d  38011  aov0nbovbi  38077  fnotaovb  38080  rexxfrd2  38371  mgmhmpropd  38533  rngcsect  38730  rngcsectALTV  38742  ringcsect  38781  ringcsectALTV  38805  lindslinindsimp2lem5  39005