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  1360  3orim123d  1361  hbbid  1628  spsbim  1896  moim  2151  moimv  2153  2euswapdc  2178  nelcon3d  2526  ralim  2609  ralimdaa  2616  ralimdv2  2620  rexim  2644  reximdv2  2649  rmoim  3027  ssel  3242  sstr2  3255  ssrexf  3310  ssrmof  3311  sscon  3363  ssdif  3364  unss1  3398  ssrin  3456  sspw  3698  prel12  3891  uniss  3951  ssuni  3952  intss  3986  intssunim  3987  iunss1  4018  iinss1  4019  ss2iun  4022  disjss2  4104  disjss1  4107  ssbrd  4168  sspwb  4351  poss  4438  pofun  4452  soss  4454  sess1  4477  sess2  4478  ordwe  4718  wessep  4720  peano2  4737  finds  4742  finds2  4743  relss  4857  ssrel  4858  ssrel2  4860  ssrelrel  4870  xpsspw  4882  relop  4925  cnvss  4948  dmss  4975  dmcosseq  5049  funss  5391  imadif  5456  imain  5458  fss  5541  fun  5556  brprcneu  5683  isores3  6011  isopolem  6018  isosolem  6020  tposfn2  6527  tposfo2  6528  tposf1o2  6531  smores  6553  tfr1onlemaccex  6609  tfrcllemaccex  6622  iinerm  6871  xpdom2  7119  ssenen  7142  exmidpw  7205  exmidpweq  7206  nnnninfeq2  7459  recexprlemlol  7983  recexprlemupu  7985  axpre-ltwlin  8240  axpre-apti  8242  nnindnn  8250  nnind  9299  uzind  9736  hashfacen  11262  pfxccatin12lem2  11481  cau3lem  11858  tgcl  15088  epttop  15114  txcnp  15295  plycj  15785  gausslemma2dlem0i  16090  gausslemma2dlem1a  16091  nnnninfex  16970