Theorem 3bitr4g 566

Description: More general version of 3bitr4i 190. 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 543	. 2 |- (ph -> (th <-> ch))
4		3bitr4g.3	. 2 |- (ta <-> ch)
5	3, 4	syl6bbr 549	1 |- (ph -> (th <-> ta))

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

This theorem is referenced by:  imbi1d 624  orbi2d 625  orbi1d 626  anbi1d 628  bibi2d 629  bibi1d 630  pm5.32rd 659  3orbi123d 904  3anbi123d 905  drex1 1198  drsb1 1217  cbvexd 1363  sbal2 1400  eubid 1427  mobid 1446  eqeq1 1528  eqeq2 1531  eleq1 1581  eleq2 1582  neeq1 1637  neeq2 1638  neleq1 1689  neleq2 1690  ralbida 1704  rexbida 1705  ralbidv2 1712  rexbidv2 1713  r19.21t 1762  reubidva 1826  raleq1f 1830  rexeq1f 1831  reueq1f 1832  eueq3 1966  dfsbcq 1990  psseq1 2186  psseq2 2187  ssconb 2221  uneq1 2228  ineq1 2261  reuun2 2329  reldisj 2365  undif4 2377  disjssun 2378  intmin4 2613  iindif2 2666  iununi 2671  breq 2676  breq1 2677  breq2 2678  brprc 2716  treq 2741  opeqex 2854  poeq1 2898  soeq1 2909  rexxfrd 2955  rabxfr 2959  iunpw 2971  freq1 2979  weeq1 2994  weeq2 2995  ordeq 3012  limeq 3017  ordunisssuc 3140  tfinds 3218  opthprc 3278  brinxp2 3288  releq 3300  eqrel 3307  brcnvg 3354  resieq 3433  cores 3556  imadif 3631  fneq1 3639  fneq2 3640  feq1 3677  feq2 3678  feq3 3679  feq23 3680  f1eq1 3717  f1eq2 3718  f1eq3 3719  foeq1 3725  foeq2 3726  foeq3 3727  f1oeq1 3741  f1oeq2 3742  f1oeq3 3743  dffo3 3876  f1fv 3931  cbvfo 3943  cbvexfo 3944  isoeq1 3945  isoeq2 3946  isoeq3 3947  isoeq4 3948  isoeq5 3949  isomin 3957  isowe 3961  2ndconst 4155  dfoprab5 4173  ereq 4325  erthi 4339  erthdmr 4342  0sdomg 4529  nnsdomo 4586  enfi 4598  isfinite2 4609  brdom7disj 4866  brdom6disj 4867  cardsdom 4901  aleph11 4944  alephiso 4957  ltapq 5141  ltmpq 5142  genpass 5177  distrlem1pr 5192  1idpr 5198  ltasr 5274  ltsor 5326  ltxr 5560  muln0b 5762  le2msqi 5942  msq11i 5943  rpneg 6125  infm3 6136  infmsup 6150  supxrre 6165  dfuzi 6287  icounlem 6438  nn0ennn 7589  znnen 7594  eltopsp 7695  istps2 7698  clsval2 7770  ocin 9252  pjtheu 9319  chpsscon3 9509  pjimai 10187  elat2 10351  mdsymi 10422

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 154  df-an 232

Copyright terms: Public domain