Theorem 3bitr4g 553

Description: More general version of 3bitr4 183. Useful for converting definitions in a formula.

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.1	. . 3 |- (ph -> (ps <-> ch))
2		3bitr4g.2	. . 3 |- (th <-> ps)
3	1, 2	syl5bb 530	. 2 |- (ph -> (th <-> ch))
4		3bitr4g.3	. 2 |- (ta <-> ch)
5	3, 4	syl6bbr 536	1 |- (ph -> (th <-> ta))

Syntax hints:   -> wi 3   <-> wb 146

This theorem is referenced by:  imbi1d 611  orbi2d 612  orbi1d 613  anbi1d 615  bibi2d 616  bibi1d 617  pm5.32rd 646  3orbi123d 889  3anbi123d 890  drex1 1152  drsb1 1171  cbvexd 1316  sbal2 1351  eubid 1378  mobid 1397  eqeq1 1473  eqeq2 1476  eleq1 1526  eleq2 1527  neeq1 1582  neeq2 1583  neleq1 1634  neleq2 1635  ralbida 1649  rexbida 1650  ralbidv2 1657  rexbidv2 1658  r19.21t 1707  reubidva 1771  raleq1f 1775  rexeq1f 1776  reueq1f 1777  eueq3 1910  dfsbcq 1933  psseq1 2125  psseq2 2126  ssconb 2160  uneq1 2167  ineq1 2200  reuun2 2268  reldisj 2303  undif4 2315  disjssun 2316  intmin4 2549  iindif2 2601  iununi 2606  breq 2611  breq1 2612  breq2 2613  brprc 2651  treq 2676  poeq1 2833  soeq1 2844  rexxfrd 2888  rabxfr 2892  iunpw 2904  freq1 2912  weeq1 2927  weeq2 2928  ordeq 2945  limeq 2950  ordunisssuc 3073  tfinds 3151  opthprc 3211  brinxp2 3221  releq 3233  eqrel 3240  brcnvg 3286  resieq 3360  cores 3485  imadif 3560  fneq1 3568  fneq2 3569  feq1 3606  feq2 3607  feq3 3608  feq23 3609  f1eq1 3645  f1eq2 3646  f1eq3 3647  foeq1 3653  foeq2 3654  foeq3 3655  f1oeq1 3669  f1oeq2 3670  f1oeq3 3671  dffo3 3804  f1fv 3859  cbvfo 3870  cbvexfo 3871  isoeq1 3872  isoeq2 3873  isoeq3 3874  isoeq4 3875  isoeq5 3876  isomin 3884  isowe 3888  2ndconst 4081  dfoprab5 4099  ereq 4251  erthi 4265  erthdmr 4268  0sdomg 4446  nnsdomo 4501  isfinite2 4523  brdom7disj 4776  brdom6disj 4777  cardsdom 4809  aleph11 4851  alephiso 4864  ltapq 5048  ltmpq 5049  genpass 5084  distrlem1pr 5099  1idpr 5105  ltasr 5181  ltsor 5233  ltxrt 5467  muln0bt 5666  le2msq 5830  msq11 5831  infm3 6001  infmsup 6015  supxrre 6030  dfuz 6150  icounlem 6345  nn0ennn 7439  eltopsp 7546  istps2 7549  clsval2 7627  ocin 9085  pjtheut 9151  chpsscon3t 9341  pjima 10015  elat2 10175  mdsym 10246

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain