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  3005  ssel  3219  sstr2  3232  ssrexf  3287  ssrmof  3288  sscon  3339  ssdif  3340  unss1  3374  ssrin  3430  prel12  3852  uniss  3912  ssuni  3913  intss  3947  intssunim  3948  iunss1  3979  iinss1  3980  ss2iun  3983  disjss2  4065  disjss1  4068  ssbrd  4129  sspwb  4306  poss  4393  pofun  4407  soss  4409  sess1  4432  sess2  4433  ordwe  4672  wessep  4674  peano2  4691  finds  4696  finds2  4697  relss  4811  ssrel  4812  ssrel2  4814  ssrelrel  4824  xpsspw  4836  relop  4878  cnvss  4901  dmss  4928  dmcosseq  5002  funss  5343  imadif  5407  imain  5409  fss  5491  fun  5505  brprcneu  5628  isores3  5951  isopolem  5958  isosolem  5960  tposfn2  6427  tposfo2  6428  tposf1o2  6431  smores  6453  tfr1onlemaccex  6509  tfrcllemaccex  6522  iinerm  6771  xpdom2  7010  ssenen  7032  exmidpw  7093  exmidpweq  7094  nnnninfeq2  7319  recexprlemlol  7836  recexprlemupu  7838  axpre-ltwlin  8093  axpre-apti  8095  nnindnn  8103  nnind  9149  uzind  9581  hashfacen  11090  pfxccatin12lem2  11302  cau3lem  11665  tgcl  14778  epttop  14804  txcnp  14985  plycj  15475  gausslemma2dlem0i  15776  gausslemma2dlem1a  15777  nnnninfex  16560