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  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  3756  uniss  3815  ssuni  3816  intss  3850  intssunim  3851  iunss1  3882  iinss1  3883  ss2iun  3886  disjss2  3967  disjss1  3970  ssbrd  4030  sspwb  4199  poss  4281  pofun  4295  soss  4297  sess1  4320  sess2  4321  ordwe  4558  wessep  4560  peano2  4577  finds  4582  finds2  4583  relss  4696  ssrel  4697  ssrel2  4699  ssrelrel  4709  xpsspw  4721  relop  4759  cnvss  4782  dmss  4808  dmcosseq  4880  funss  5215  imadif  5276  imain  5278  fss  5357  fun  5368  brprcneu  5487  isores3  5792  isopolem  5799  isosolem  5801  tposfn2  6243  tposfo2  6244  tposf1o2  6247  smores  6269  tfr1onlemaccex  6325  tfrcllemaccex  6338  iinerm  6583  xpdom2  6807  ssenen  6827  exmidpw  6884  exmidpweq  6885  nnnninfeq2  7103  recexprlemlol  7581  recexprlemupu  7583  axpre-ltwlin  7838  axpre-apti  7840  nnindnn  7848  nnind  8887  uzind  9316  hashfacen  10764  cau3lem  11071  tgcl  12823  epttop  12849  txcnp  13030