Theorem 3imtr4g 203

Description: More general version of 3imtr4i 199. 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 150	. 2 ⊢ (𝜑 → (𝜃 → 𝜒))
4		3imtr4g.3	. 2 ⊢ (𝜏 ↔ 𝜒)
5	3, 4	syl6ibr 160	1 ⊢ (𝜑 → (𝜃 → 𝜏))

Syntax hints:   → wi 4   ↔ wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  3anim123d  1251  3orim123d  1252  hbbid  1508  spsbim  1766  moim  2007  moimv  2009  2euswapdc  2034  ralim  2427  ralimdaa  2433  ralimdv2  2436  rexim  2460  reximdv2  2465  rmoim  2800  ssel  3002  sstr2  3015  sscon  3116  ssdif  3117  unss1  3151  ssrin  3207  prel12  3583  uniss  3642  ssuni  3643  intss  3677  intssunim  3678  iunss1  3709  iinss1  3710  ss2iun  3713  disjss2  3789  disjss1  3792  ssbrd  3846  sspwb  3999  poss  4081  pofun  4095  soss  4097  sess1  4120  sess2  4121  ordwe  4346  wessep  4348  peano2  4364  finds  4369  finds2  4370  relss  4473  ssrel  4474  ssrel2  4476  ssrelrel  4486  xpsspw  4498  relop  4534  cnvss  4556  dmss  4582  dmcosseq  4651  funss  4970  imadif  5030  imain  5032  fss  5105  fun  5114  brprcneu  5223  isores3  5507  isopolem  5513  isosolem  5515  tposfn2  5936  tposfo2  5937  tposf1o2  5940  smores  5962  tfr1onlemaccex  6018  tfrcllemaccex  6031  iinerm  6266  xpdom2  6397  recexprlemlol  6948  recexprlemupu  6950  axpre-ltwlin  7181  axpre-apti  7183  nnindnn  7191  nnind  8192  uzind  8609  cau3lem  10219