Theorem 3imtr4g 194

Description: More general version of 3imtr4i 190. 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 141	. 2 |- ( ph -> ( th -> ch ) )
4		3imtr4g.3	. 2 |- ( ta <-> ch )
5	3, 4	syl6ibr 151	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:  3anim123d  1214  3orim123d  1215  hbbid  1467  spsbim  1724  moim  1964  moimv  1966  2euswapdc  1991  ralim  2380  ralimdaa  2386  ralimdv2  2389  rexim  2413  reximdv2  2418  rmoim  2740  ssel  2939  sstr2  2952  sscon  3077  ssdif  3078  unss1  3112  ssrin  3162  prel12  3542  uniss  3601  ssuni  3602  intss  3636  intssunim  3637  iunss1  3668  iinss1  3669  ss2iun  3672  disjss2  3748  disjss1  3751  ssbrd  3805  sspwb  3952  poss  4035  pofun  4049  soss  4051  sess1  4074  sess2  4075  ordwe  4300  wessep  4302  peano2  4318  finds  4323  finds2  4324  relss  4427  ssrel  4428  ssrel2  4430  ssrelrel  4440  xpsspw  4450  relop  4486  cnvss  4508  dmss  4534  dmcosseq  4603  funss  4920  imadif  4979  imain  4981  fss  5054  fun  5063  brprcneu  5171  isores3  5455  isopolem  5461  isosolem  5463  tposfn2  5881  tposfo2  5882  tposf1o2  5885  smores  5907  iinerm  6178  xpdom2  6305  recexprlemlol  6724  recexprlemupu  6726  axpre-ltwlin  6957  axpre-apti  6959  nnindnn  6967  nnind  7930  uzind  8349  cau3lem  9710