Theorem 3bitr4g 428

Description: More general version of 3bitr4 158. 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 410	. 2 |- (ph -> (th <-> ch))
4		3bitr4g.3	. 2 |- (ta <-> ch)
5	3, 4	syl6bbr 416	1 |- (ph -> (th <-> ta ))

Syntax hints:   -> wi 2   <-> wb 127

This theorem is referenced by:  imbi1d 465  orbi2d 466  orbi1d 467  anbi1d 469  bibi2d 470  bibi1d 471  pm5.32rd 492  bi3ord 635  bi3and 636  cbvexd 978  sbal2 1005  bieud 1012  bimod 1030  cleq1 1107  cleq2 1110  eleq1 1149  eleq2 1150  neeq1 1194  neeq2 1195  neleq1 1199  neleq2 1200  biralda 1213  birexda 1214  biraldv2 1221  birexdv2 1222  bireudva 1317  raleqf 1321  rexeqf 1322  reueqf 1323  eueq3 1430  dfsbcq 1442  psseq1 1559  psseq2 1560  ssconb 1598  uneq1 1605  ineq1 1638  undif4 1744  iindif2 2033  iununi 2037  iunpw 2040  treq 2047  breq 2064  breq1 2065  breq2 2066  brprc 2097  poeq1 2130  soeq1 2141  freq1 2174  weeq1 2189  weeq2 2190  ordeq 2206  limeq 2211  ordunisssuc 2334  tfinds 2401  opelxpex 2445  opthprc 2457  releq 2477  cleqrel 2483  cores 2659  imadif 2714  fneq1 2718  fneq2 2719  feq1 2748  feq2 2749  feq3 2750  f1eq1 2776  f1eq2 2777  f1eq3 2778  foeq1 2784  foeq2 2785  foeq3 2786  f1oeq1 2795  f1oeq2 2796  f1oeq3 2797  fvelrn 2883  f1fv 2916  cbvfo 2923  cbvexfo 2924  isoeq1 2925  isoeq2 2926  isoeq3 2927  isoeq4 2928  isoeq5 2929  isomin 2937  isowe 2941  ereq 3206  erthi 3218  erthdmr 3221  nnsdomo 3417  isfinite2 3437  cardsdom 3643  aleph11 3684  alephiso 3697  ltapq 3870  ltmpq 3871  genpass 3906  distrlem1pr 3921  1idpr 3927  ltasr 4003  ltsor 4055  muln0bt 4213  divneq0bt 4230  lemul2 4396  le2sq 4415  sq11 4416  nn0ennn 4925  ocin 5177  pjthut 5243  chpsscon3t 5420  elat2 5739

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

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org