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	⊢ (𝜑 → (𝜓 → 𝜒))
3imtr4g.2	⊢ (𝜃 ↔ 𝜓)
3imtr4g.3	⊢ (𝜏 ↔ 𝜒)

Assertion

Ref	Expression
3imtr4g	⊢ (𝜑 → (𝜃 → 𝜏))

Proof of Theorem 3imtr4g

Step	Hyp	Ref	Expression
1		3imtr4g.2	. . 3 ⊢ (𝜃 ↔ 𝜓)
2		3imtr4g.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	biimtrid 152	. 2 ⊢ (𝜑 → (𝜃 → 𝜒))
4		3imtr4g.3	. 2 ⊢ (𝜏 ↔ 𝜒)
5	3, 4	imbitrrdi 162	1 ⊢ (𝜑 → (𝜃 → 𝜏))

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  2962  ssel  3174  sstr2  3187  ssrexf  3242  ssrmof  3243  sscon  3294  ssdif  3295  unss1  3329  ssrin  3385  prel12  3798  uniss  3857  ssuni  3858  intss  3892  intssunim  3893  iunss1  3924  iinss1  3925  ss2iun  3928  disjss2  4010  disjss1  4013  ssbrd  4073  sspwb  4246  poss  4330  pofun  4344  soss  4346  sess1  4369  sess2  4370  ordwe  4609  wessep  4611  peano2  4628  finds  4633  finds2  4634  relss  4747  ssrel  4748  ssrel2  4750  ssrelrel  4760  xpsspw  4772  relop  4813  cnvss  4836  dmss  4862  dmcosseq  4934  funss  5274  imadif  5335  imain  5337  fss  5416  fun  5427  brprcneu  5548  isores3  5859  isopolem  5866  isosolem  5868  tposfn2  6321  tposfo2  6322  tposf1o2  6325  smores  6347  tfr1onlemaccex  6403  tfrcllemaccex  6416  iinerm  6663  xpdom2  6887  ssenen  6909  exmidpw  6966  exmidpweq  6967  nnnninfeq2  7190  recexprlemlol  7688  recexprlemupu  7690  axpre-ltwlin  7945  axpre-apti  7947  nnindnn  7955  nnind  9000  uzind  9431  hashfacen  10910  cau3lem  11261  tgcl  14243  epttop  14269  txcnp  14450  plycj  14939  gausslemma2dlem0i  15214  gausslemma2dlem1a  15215