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  1332  3orim123d  1333  hbbid  1598  spsbim  1866  moim  2118  moimv  2120  2euswapdc  2145  nelcon3d  2482  ralim  2565  ralimdaa  2572  ralimdv2  2576  rexim  2600  reximdv2  2605  rmoim  2974  ssel  3187  sstr2  3200  ssrexf  3255  ssrmof  3256  sscon  3307  ssdif  3308  unss1  3342  ssrin  3398  prel12  3812  uniss  3871  ssuni  3872  intss  3906  intssunim  3907  iunss1  3938  iinss1  3939  ss2iun  3942  disjss2  4024  disjss1  4027  ssbrd  4087  sspwb  4260  poss  4345  pofun  4359  soss  4361  sess1  4384  sess2  4385  ordwe  4624  wessep  4626  peano2  4643  finds  4648  finds2  4649  relss  4762  ssrel  4763  ssrel2  4765  ssrelrel  4775  xpsspw  4787  relop  4828  cnvss  4851  dmss  4877  dmcosseq  4950  funss  5290  imadif  5354  imain  5356  fss  5437  fun  5448  brprcneu  5569  isores3  5884  isopolem  5891  isosolem  5893  tposfn2  6352  tposfo2  6353  tposf1o2  6356  smores  6378  tfr1onlemaccex  6434  tfrcllemaccex  6447  iinerm  6694  xpdom2  6926  ssenen  6948  exmidpw  7005  exmidpweq  7006  nnnninfeq2  7231  recexprlemlol  7739  recexprlemupu  7741  axpre-ltwlin  7996  axpre-apti  7998  nnindnn  8006  nnind  9052  uzind  9484  hashfacen  10981  cau3lem  11425  tgcl  14536  epttop  14562  txcnp  14743  plycj  15233  gausslemma2dlem0i  15534  gausslemma2dlem1a  15535  nnnninfex  15959