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  1353  3orim123d  1354  hbbid  1621  spsbim  1889  moim  2142  moimv  2144  2euswapdc  2169  nelcon3d  2506  ralim  2589  ralimdaa  2596  ralimdv2  2600  rexim  2624  reximdv2  2629  rmoim  3004  ssel  3218  sstr2  3231  ssrexf  3286  ssrmof  3287  sscon  3338  ssdif  3339  unss1  3373  ssrin  3429  prel12  3849  uniss  3909  ssuni  3910  intss  3944  intssunim  3945  iunss1  3976  iinss1  3977  ss2iun  3980  disjss2  4062  disjss1  4065  ssbrd  4126  sspwb  4302  poss  4389  pofun  4403  soss  4405  sess1  4428  sess2  4429  ordwe  4668  wessep  4670  peano2  4687  finds  4692  finds2  4693  relss  4806  ssrel  4807  ssrel2  4809  ssrelrel  4819  xpsspw  4831  relop  4872  cnvss  4895  dmss  4922  dmcosseq  4996  funss  5337  imadif  5401  imain  5403  fss  5485  fun  5497  brprcneu  5620  isores3  5939  isopolem  5946  isosolem  5948  tposfn2  6412  tposfo2  6413  tposf1o2  6416  smores  6438  tfr1onlemaccex  6494  tfrcllemaccex  6507  iinerm  6754  xpdom2  6990  ssenen  7012  exmidpw  7070  exmidpweq  7071  nnnninfeq2  7296  recexprlemlol  7813  recexprlemupu  7815  axpre-ltwlin  8070  axpre-apti  8072  nnindnn  8080  nnind  9126  uzind  9558  hashfacen  11058  pfxccatin12lem2  11263  cau3lem  11625  tgcl  14738  epttop  14764  txcnp  14945  plycj  15435  gausslemma2dlem0i  15736  gausslemma2dlem1a  15737  nnnninfex  16388