Theorem 3bitr4g 279

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

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

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 177

This theorem is referenced by:  bibi1d  310  pm5.32rd  621  orbi2d  682  orbi1d  683  3orbi123d  1251  3anbi123d  1252  nanbi1  1295  nanbi2  1296  xorbi12d  1315  hadbi123d  1382  cadbi123d  1383  cad1  1398  had0  1403  nfbidf  1774  drex1  1967  drnf1  1969  drnf2  1970  cbvexd  2009  drsb1  2022  sbal2  2134  eujustALT  2207  eubid  2211  mobid  2238  eqeq1  2359  eqeq2  2362  eleq1  2413  eleq2  2414  nfceqdf  2489  drnfc1  2506  drnfc2  2507  neeq1  2525  neeq2  2526  neleq1  2608  neleq2  2609  ralbida  2629  rexbida  2630  ralbidv2  2637  rexbidv2  2638  r19.21t  2700  r19.23t  2729  ralcom2  2776  reubida  2794  rmobida  2799  raleqf  2804  rexeqf  2805  reueq1f  2806  rmoeq1f  2807  cbvraldva2  2840  cbvrexdva2  2841  dfsbcq  3049  sbcbid  3100  sbcrext  3120  sbcabel  3124  sbnfc2  3197  elin  3220  elun  3221  psseq1  3357  psseq2  3358  ssconb  3400  uneq1  3412  ineq1  3451  difin2  3517  reuun2  3539  reldisj  3595  undif4  3608  disjssun  3609  pssdifcom1  3636  pssdifcom2  3637  sbcss  3661  eltpg  3770  raltpg  3778  rextpg  3779  intmin4  3956  dfiun2g  4000  iindif2  4036  iinin2  4037  iinxprg  4044  ssofeq  4078  xpkeq1  4199  xpkeq2  4200  opkelimagekg  4272  iotaeq  4348  sniota  4370  sfineq1  4527  sfineq2  4528  phialllem1  4617  breq  4642  breq1  4643  breq2  4644  elimasn  5020  dfco2a  5082  imadif  5172  fneq1  5174  fneq2  5175  feq1  5211  feq2  5212  feq3  5213  fcnvres  5244  f1eq1  5254  f1eq2  5255  f1eq3  5256  foeq1  5266  foeq2  5267  foeq3  5268  f1oeq1  5282  f1oeq2  5283  f1oeq3  5284  fun11iun  5306  dmfco  5382  dffo3  5423  funiunfv  5468  dff13  5472  isoeq1  5483  isoeq2  5484  isoeq3  5485  isoeq4  5486  isoeq5  5487  isomin  5497  mpt2eq123  5662  clos1basesucg  5885  erdmrn  5966  ereldm  5972  ce0nnul  6178  nmembers1lem3  6271  epelcres  6329