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  1330  3orim123d  1331  hbbid  1586  spsbim  1854  moim  2106  moimv  2108  2euswapdc  2133  nelcon3d  2470  ralim  2553  ralimdaa  2560  ralimdv2  2564  rexim  2588  reximdv2  2593  rmoim  2961  ssel  3173  sstr2  3186  ssrexf  3241  ssrmof  3242  sscon  3293  ssdif  3294  unss1  3328  ssrin  3384  prel12  3797  uniss  3856  ssuni  3857  intss  3891  intssunim  3892  iunss1  3923  iinss1  3924  ss2iun  3927  disjss2  4009  disjss1  4012  ssbrd  4072  sspwb  4245  poss  4329  pofun  4343  soss  4345  sess1  4368  sess2  4369  ordwe  4608  wessep  4610  peano2  4627  finds  4632  finds2  4633  relss  4746  ssrel  4747  ssrel2  4749  ssrelrel  4759  xpsspw  4771  relop  4812  cnvss  4835  dmss  4861  dmcosseq  4933  funss  5273  imadif  5334  imain  5336  fss  5415  fun  5426  brprcneu  5547  isores3  5858  isopolem  5865  isosolem  5867  tposfn2  6319  tposfo2  6320  tposf1o2  6323  smores  6345  tfr1onlemaccex  6401  tfrcllemaccex  6414  iinerm  6661  xpdom2  6885  ssenen  6907  exmidpw  6964  exmidpweq  6965  nnnninfeq2  7188  recexprlemlol  7686  recexprlemupu  7688  axpre-ltwlin  7943  axpre-apti  7945  nnindnn  7953  nnind  8998  uzind  9428  hashfacen  10907  cau3lem  11258  tgcl  14232  epttop  14258  txcnp  14439  gausslemma2dlem0i  15173  gausslemma2dlem1a  15174