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  1355  3orim123d  1356  hbbid  1623  spsbim  1891  moim  2144  moimv  2146  2euswapdc  2171  nelcon3d  2508  ralim  2591  ralimdaa  2598  ralimdv2  2602  rexim  2626  reximdv2  2631  rmoim  3007  ssel  3221  sstr2  3234  ssrexf  3289  ssrmof  3290  sscon  3341  ssdif  3342  unss1  3376  ssrin  3432  prel12  3854  uniss  3914  ssuni  3915  intss  3949  intssunim  3950  iunss1  3981  iinss1  3982  ss2iun  3985  disjss2  4067  disjss1  4070  ssbrd  4131  sspwb  4308  poss  4395  pofun  4409  soss  4411  sess1  4434  sess2  4435  ordwe  4674  wessep  4676  peano2  4693  finds  4698  finds2  4699  relss  4813  ssrel  4814  ssrel2  4816  ssrelrel  4826  xpsspw  4838  relop  4880  cnvss  4903  dmss  4930  dmcosseq  5004  funss  5345  imadif  5410  imain  5412  fss  5494  fun  5508  brprcneu  5632  isores3  5955  isopolem  5962  isosolem  5964  tposfn2  6431  tposfo2  6432  tposf1o2  6435  smores  6457  tfr1onlemaccex  6513  tfrcllemaccex  6526  iinerm  6775  xpdom2  7014  ssenen  7036  exmidpw  7099  exmidpweq  7100  nnnninfeq2  7327  recexprlemlol  7845  recexprlemupu  7847  axpre-ltwlin  8102  axpre-apti  8104  nnindnn  8112  nnind  9158  uzind  9590  hashfacen  11099  pfxccatin12lem2  11311  cau3lem  11674  tgcl  14787  epttop  14813  txcnp  14994  plycj  15484  gausslemma2dlem0i  15785  gausslemma2dlem1a  15786  nnnninfex  16624