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	⊢ (𝜑 → (𝜓 → 𝜒))
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	syl5bi 151	. 2 ⊢ (𝜑 → (𝜃 → 𝜒))
4		3imtr4g.3	. 2 ⊢ (𝜏 ↔ 𝜒)
5	3, 4	syl6ibr 161	1 ⊢ (𝜑 → (𝜃 → 𝜏))

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  1298  3orim123d  1299  hbbid  1555  spsbim  1816  moim  2064  moimv  2066  2euswapdc  2091  nelcon3d  2415  ralim  2494  ralimdaa  2501  ralimdv2  2505  rexim  2529  reximdv2  2534  rmoim  2889  ssel  3096  sstr2  3109  ssrexf  3164  ssrmof  3165  sscon  3215  ssdif  3216  unss1  3250  ssrin  3306  prel12  3706  uniss  3765  ssuni  3766  intss  3800  intssunim  3801  iunss1  3832  iinss1  3833  ss2iun  3836  disjss2  3917  disjss1  3920  ssbrd  3979  sspwb  4146  poss  4228  pofun  4242  soss  4244  sess1  4267  sess2  4268  ordwe  4498  wessep  4500  peano2  4517  finds  4522  finds2  4523  relss  4634  ssrel  4635  ssrel2  4637  ssrelrel  4647  xpsspw  4659  relop  4697  cnvss  4720  dmss  4746  dmcosseq  4818  funss  5150  imadif  5211  imain  5213  fss  5292  fun  5303  brprcneu  5422  isores3  5724  isopolem  5731  isosolem  5733  tposfn2  6171  tposfo2  6172  tposf1o2  6175  smores  6197  tfr1onlemaccex  6253  tfrcllemaccex  6266  iinerm  6509  xpdom2  6733  ssenen  6753  exmidpw  6810  recexprlemlol  7458  recexprlemupu  7460  axpre-ltwlin  7715  axpre-apti  7717  nnindnn  7725  nnind  8760  uzind  9186  hashfacen  10611  cau3lem  10918  tgcl  12272  epttop  12298  txcnp  12479