Theorem 3bitr4g 212

Description: More general version of 3bitr4i 201. Useful for converting definitions in a formula. (Contributed by NM, 5-Aug-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 181	. 2 |- (ph -> (th <-> ch))
4		3bitr4g.3	. 2 |- (ta <-> ch)
5	3, 4	syl6bbr 187	1 |- (ph -> (th <-> ta))

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  bibi1d  222  pm5.32rd  424  orbi1d  704  dcbid  747  pm4.14dc  786  orbididc  859  3orbi123d  1205  3anbi123d  1206  xorbi2d  1269  xorbi1d  1270  nfbidf  1429  drnf1  1618  drnf2  1619  drsb1  1677  sbal2  1895  eubidh  1903  eubid  1904  mobidh  1931  mobid  1932  eqeq1  2043  eqeq2  2046  eleq1  2097  eleq2  2098  nfceqdf  2174  drnfc1  2191  drnfc2  2192  neeq1  2213  neeq2  2214  neleq1  2295  neleq2  2296  ralbida  2314  rexbida  2315  ralbidv2  2322  rexbidv2  2323  r19.21t  2388  r19.23t  2417  reubida  2485  rmobida  2490  raleqf  2495  rexeqf  2496  reueq1f  2497  rmoeq1f  2498  cbvraldva2  2531  cbvrexdva2  2532  dfsbcq  2760  sbcbid  2810  sbcabel  2833  sbnfc2  2900  psseq1  3025  psseq2  3026  ssconb  3070  uneq1  3084  ineq1  3125  difin2  3193  reuun2  3214  reldisj  3265  undif4  3278  disjssun  3279  sbcssg  3324  eltpg  3407  raltpg  3414  rextpg  3415  opeq1  3540  opeq2  3541  intmin4  3634  dfiun2g  3680  iindif2m  3715  iinin2m  3716  breq  3757  breq1  3758  breq2  3759  treq  3851  opthg2  3967  poeq1  4027  soeq1  4043  ordeq  4075  limeq  4080  rabxfrd  4167  iunpw  4177  opthprc  4334  releq  4365  sbcrel  4369  eqrel  4372  eqrelrel  4384  xpiindim  4416  brcnvg  4459  brresg  4563  resieq  4565  xpcanm  4703  xpcan2m  4704  dmsnopg  4735  dfco2a  4764  cnvpom  4803  cnvsom  4804  iotaeq  4818  sniota  4837  sbcfung  4868  fneq1  4930  fneq2  4931  feq1  4973  feq2  4974  feq3  4975  sbcfng  4987  sbcfg  4988  f1eq1  5030  f1eq2  5031  f1eq3  5032  foeq1  5045  foeq2  5046  foeq3  5047  f1oeq1  5060  f1oeq2  5061  f1oeq3  5062  fun11iun  5090  mpteqb  5204  dffo3  5257  fmptco  5273  dff13  5350  f1imaeq  5357  f1imapss  5358  f1eqcocnv  5374  fliftcnv  5378  isoeq1  5384  isoeq2  5385  isoeq3  5386  isoeq4  5387  isoeq5  5388  isocnv2  5395  acexmid  5454  fnotovb  5490  mpt2eq123  5506  ottposg  5811  dmtpos  5812  smoeq  5846  nnacan  6021  nnmcan  6028  ereq1  6049  ereq2  6050  elecg  6080  ereldm  6085  enfi  6252  creur  7672  eqreznegel  8305  ltxr  8445  icoshftf1o  8609  elfzm11  8703  elfzomelpfzo  8837  nn0ennn  8870  nnesq  9001  cbvrald  9242  bj-dcbi  9359