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  1314  3orim123d  1315  hbbid  1568  spsbim  1836  moim  2083  moimv  2085  2euswapdc  2110  nelcon3d  2446  ralim  2529  ralimdaa  2536  ralimdv2  2540  rexim  2564  reximdv2  2569  rmoim  2931  ssel  3141  sstr2  3154  ssrexf  3209  ssrmof  3210  sscon  3261  ssdif  3262  unss1  3296  ssrin  3352  prel12  3758  uniss  3817  ssuni  3818  intss  3852  intssunim  3853  iunss1  3884  iinss1  3885  ss2iun  3888  disjss2  3969  disjss1  3972  ssbrd  4032  sspwb  4201  poss  4283  pofun  4297  soss  4299  sess1  4322  sess2  4323  ordwe  4560  wessep  4562  peano2  4579  finds  4584  finds2  4585  relss  4698  ssrel  4699  ssrel2  4701  ssrelrel  4711  xpsspw  4723  relop  4761  cnvss  4784  dmss  4810  dmcosseq  4882  funss  5217  imadif  5278  imain  5280  fss  5359  fun  5370  brprcneu  5489  isores3  5794  isopolem  5801  isosolem  5803  tposfn2  6245  tposfo2  6246  tposf1o2  6249  smores  6271  tfr1onlemaccex  6327  tfrcllemaccex  6340  iinerm  6585  xpdom2  6809  ssenen  6829  exmidpw  6886  exmidpweq  6887  nnnninfeq2  7105  recexprlemlol  7588  recexprlemupu  7590  axpre-ltwlin  7845  axpre-apti  7847  nnindnn  7855  nnind  8894  uzind  9323  hashfacen  10771  cau3lem  11078  tgcl  12858  epttop  12884  txcnp  13065