Theorem 3imtr4g 261

Description: More general version of 3imtr4i 257. Useful for converting definitions in a formula. (Contributed by NM, 20-May-1996.) (Proof shortened by Wolf Lammen, 20-Dec-2013.)

Hypotheses

Ref	Expression
3imtr4g.1	|- (ph -> (ps -> ch))
3imtr4g.2	|- (th <-> ps)
3imtr4g.3	|- (ta <-> ch)

Assertion

Ref	Expression
3imtr4g	|- (ph -> (th -> ta))

Proof of Theorem 3imtr4g

Step	Hyp	Ref	Expression
1		3imtr4g.2	. . 3 |- (th <-> ps)
2		3imtr4g.1	. . 3 |- (ph -> (ps -> ch))
3	1, 2	syl5bi 208	. 2 |- (ph -> (th -> ch))
4		3imtr4g.3	. 2 |- (ta <-> ch)
5	3, 4	syl6ibr 218	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:  3anim123d  1259  3orim123d  1260  moim  2250  morimv  2252  2euswap  2280  ralim  2686  ralimdaa  2692  ralimdv2  2695  rexim  2719  reximdv2  2724  moeq3  3014  rmoim  3036  2reuswap  3039  ssel  3268  sstr2  3280  sscon  3401  ssdif  3402  unss1  3433  ssrin  3481  difin0ss  3617  r19.2z  3640  uniss  3913  ssuni  3914  intss  3948  intssuni  3949  iunss1  3981  iinss1  3982  ss2iun  3985  sspwb  4119  findsd  4411  ncfinlower  4484  evenoddnnnul  4515  spfinsfincl  4540  vfinspss  4552  vfinspclt  4553  vinf  4556  ssbrd  4681  ssrel  4845  cnvss  4886  dmss  4907  dmcosseq  4974  funss  5127  fss  5231  fun  5237  eqfnfv  5393  clos1conn  5880  clos1is  5882  enadjlem1  6060  enprmaplem6  6082  leltctr  6213  nnltp1c  6263  nncdiv3  6278  spacind  6288  nchoicelem17  6306