Theorem 3imtr4g 205

Description: More general version of 3imtr4i 201. 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	biimtrid 152	. 2 |- ( ph -> ( th -> ch ) )
4		3imtr4g.3	. 2 |- ( ta <-> ch )
5	3, 4	imbitrrdi 162	1 |- ( ph -> ( th -> ta ) )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3anim123d  1332  3orim123d  1333  hbbid  1599  spsbim  1867  moim  2120  moimv  2122  2euswapdc  2147  nelcon3d  2484  ralim  2567  ralimdaa  2574  ralimdv2  2578  rexim  2602  reximdv2  2607  rmoim  2981  ssel  3195  sstr2  3208  ssrexf  3263  ssrmof  3264  sscon  3315  ssdif  3316  unss1  3350  ssrin  3406  prel12  3825  uniss  3885  ssuni  3886  intss  3920  intssunim  3921  iunss1  3952  iinss1  3953  ss2iun  3956  disjss2  4038  disjss1  4041  ssbrd  4102  sspwb  4278  poss  4363  pofun  4377  soss  4379  sess1  4402  sess2  4403  ordwe  4642  wessep  4644  peano2  4661  finds  4666  finds2  4667  relss  4780  ssrel  4781  ssrel2  4783  ssrelrel  4793  xpsspw  4805  relop  4846  cnvss  4869  dmss  4896  dmcosseq  4969  funss  5309  imadif  5373  imain  5375  fss  5457  fun  5469  brprcneu  5592  isores3  5907  isopolem  5914  isosolem  5916  tposfn2  6375  tposfo2  6376  tposf1o2  6379  smores  6401  tfr1onlemaccex  6457  tfrcllemaccex  6470  iinerm  6717  xpdom2  6951  ssenen  6973  exmidpw  7031  exmidpweq  7032  nnnninfeq2  7257  recexprlemlol  7774  recexprlemupu  7776  axpre-ltwlin  8031  axpre-apti  8033  nnindnn  8041  nnind  9087  uzind  9519  hashfacen  11018  pfxccatin12lem2  11222  cau3lem  11540  tgcl  14651  epttop  14677  txcnp  14858  plycj  15348  gausslemma2dlem0i  15649  gausslemma2dlem1a  15650  nnnninfex  16161