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  1598  spsbim  1866  moim  2118  moimv  2120  2euswapdc  2145  nelcon3d  2482  ralim  2565  ralimdaa  2572  ralimdv2  2576  rexim  2600  reximdv2  2605  rmoim  2974  ssel  3187  sstr2  3200  ssrexf  3255  ssrmof  3256  sscon  3307  ssdif  3308  unss1  3342  ssrin  3398  prel12  3812  uniss  3871  ssuni  3872  intss  3906  intssunim  3907  iunss1  3938  iinss1  3939  ss2iun  3942  disjss2  4024  disjss1  4027  ssbrd  4088  sspwb  4261  poss  4346  pofun  4360  soss  4362  sess1  4385  sess2  4386  ordwe  4625  wessep  4627  peano2  4644  finds  4649  finds2  4650  relss  4763  ssrel  4764  ssrel2  4766  ssrelrel  4776  xpsspw  4788  relop  4829  cnvss  4852  dmss  4878  dmcosseq  4951  funss  5291  imadif  5355  imain  5357  fss  5439  fun  5450  brprcneu  5571  isores3  5886  isopolem  5893  isosolem  5895  tposfn2  6354  tposfo2  6355  tposf1o2  6358  smores  6380  tfr1onlemaccex  6436  tfrcllemaccex  6449  iinerm  6696  xpdom2  6928  ssenen  6950  exmidpw  7007  exmidpweq  7008  nnnninfeq2  7233  recexprlemlol  7741  recexprlemupu  7743  axpre-ltwlin  7998  axpre-apti  8000  nnindnn  8008  nnind  9054  uzind  9486  hashfacen  10983  cau3lem  11458  tgcl  14569  epttop  14595  txcnp  14776  plycj  15266  gausslemma2dlem0i  15567  gausslemma2dlem1a  15568  nnnninfex  15996