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	syl6ibr 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  1319  3orim123d  1320  hbbid  1575  spsbim  1843  moim  2090  moimv  2092  2euswapdc  2117  nelcon3d  2453  ralim  2536  ralimdaa  2543  ralimdv2  2547  rexim  2571  reximdv2  2576  rmoim  2938  ssel  3149  sstr2  3162  ssrexf  3217  ssrmof  3218  sscon  3269  ssdif  3270  unss1  3304  ssrin  3360  prel12  3770  uniss  3829  ssuni  3830  intss  3864  intssunim  3865  iunss1  3896  iinss1  3897  ss2iun  3900  disjss2  3981  disjss1  3984  ssbrd  4044  sspwb  4214  poss  4296  pofun  4310  soss  4312  sess1  4335  sess2  4336  ordwe  4573  wessep  4575  peano2  4592  finds  4597  finds2  4598  relss  4711  ssrel  4712  ssrel2  4714  ssrelrel  4724  xpsspw  4736  relop  4774  cnvss  4797  dmss  4823  dmcosseq  4895  funss  5232  imadif  5293  imain  5295  fss  5374  fun  5385  brprcneu  5505  isores3  5811  isopolem  5818  isosolem  5820  tposfn2  6262  tposfo2  6263  tposf1o2  6266  smores  6288  tfr1onlemaccex  6344  tfrcllemaccex  6357  iinerm  6602  xpdom2  6826  ssenen  6846  exmidpw  6903  exmidpweq  6904  nnnninfeq2  7122  recexprlemlol  7620  recexprlemupu  7622  axpre-ltwlin  7877  axpre-apti  7879  nnindnn  7887  nnind  8929  uzind  9358  hashfacen  10807  cau3lem  11114  tgcl  13346  epttop  13372  txcnp  13553