Theorem 3imtr4g 204

Description: More general version of 3imtr4i 200. 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	syl5bi 151	. 2 |- ( ph -> ( th -> ch ) )
4		3imtr4g.3	. 2 |- ( ta <-> ch )
5	3, 4	syl6ibr 161	1 |- ( ph -> ( th -> ta ) )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3anim123d  1308  3orim123d  1309  hbbid  1562  spsbim  1830  moim  2077  moimv  2079  2euswapdc  2104  nelcon3d  2440  ralim  2523  ralimdaa  2530  ralimdv2  2534  rexim  2558  reximdv2  2563  rmoim  2922  ssel  3131  sstr2  3144  ssrexf  3199  ssrmof  3200  sscon  3251  ssdif  3252  unss1  3286  ssrin  3342  prel12  3745  uniss  3804  ssuni  3805  intss  3839  intssunim  3840  iunss1  3871  iinss1  3872  ss2iun  3875  disjss2  3956  disjss1  3959  ssbrd  4019  sspwb  4188  poss  4270  pofun  4284  soss  4286  sess1  4309  sess2  4310  ordwe  4547  wessep  4549  peano2  4566  finds  4571  finds2  4572  relss  4685  ssrel  4686  ssrel2  4688  ssrelrel  4698  xpsspw  4710  relop  4748  cnvss  4771  dmss  4797  dmcosseq  4869  funss  5201  imadif  5262  imain  5264  fss  5343  fun  5354  brprcneu  5473  isores3  5777  isopolem  5784  isosolem  5786  tposfn2  6225  tposfo2  6226  tposf1o2  6229  smores  6251  tfr1onlemaccex  6307  tfrcllemaccex  6320  iinerm  6564  xpdom2  6788  ssenen  6808  exmidpw  6865  exmidpweq  6866  nnnninfeq2  7084  recexprlemlol  7558  recexprlemupu  7560  axpre-ltwlin  7815  axpre-apti  7817  nnindnn  7825  nnind  8864  uzind  9293  hashfacen  10735  cau3lem  11042  tgcl  12605  epttop  12631  txcnp  12812