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  1297  3orim123d  1298  hbbid  1554  spsbim  1815  moim  2063  moimv  2065  2euswapdc  2090  nelcon3d  2414  ralim  2491  ralimdaa  2498  ralimdv2  2502  rexim  2526  reximdv2  2531  rmoim  2885  ssel  3091  sstr2  3104  ssrexf  3159  ssrmof  3160  sscon  3210  ssdif  3211  unss1  3245  ssrin  3301  prel12  3698  uniss  3757  ssuni  3758  intss  3792  intssunim  3793  iunss1  3824  iinss1  3825  ss2iun  3828  disjss2  3909  disjss1  3912  ssbrd  3971  sspwb  4138  poss  4220  pofun  4234  soss  4236  sess1  4259  sess2  4260  ordwe  4490  wessep  4492  peano2  4509  finds  4514  finds2  4515  relss  4626  ssrel  4627  ssrel2  4629  ssrelrel  4639  xpsspw  4651  relop  4689  cnvss  4712  dmss  4738  dmcosseq  4810  funss  5142  imadif  5203  imain  5205  fss  5284  fun  5295  brprcneu  5414  isores3  5716  isopolem  5723  isosolem  5725  tposfn2  6163  tposfo2  6164  tposf1o2  6167  smores  6189  tfr1onlemaccex  6245  tfrcllemaccex  6258  iinerm  6501  xpdom2  6725  ssenen  6745  exmidpw  6802  recexprlemlol  7434  recexprlemupu  7436  axpre-ltwlin  7691  axpre-apti  7693  nnindnn  7701  nnind  8736  uzind  9162  hashfacen  10579  cau3lem  10886  tgcl  12233  epttop  12259  txcnp  12440