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  1355  3orim123d  1356  hbbid  1623  spsbim  1891  moim  2144  moimv  2146  2euswapdc  2171  nelcon3d  2508  ralim  2591  ralimdaa  2598  ralimdv2  2602  rexim  2626  reximdv2  2631  rmoim  3007  ssel  3221  sstr2  3234  ssrexf  3289  ssrmof  3290  sscon  3341  ssdif  3342  unss1  3376  ssrin  3432  prel12  3854  uniss  3914  ssuni  3915  intss  3949  intssunim  3950  iunss1  3981  iinss1  3982  ss2iun  3985  disjss2  4067  disjss1  4070  ssbrd  4131  sspwb  4308  poss  4395  pofun  4409  soss  4411  sess1  4434  sess2  4435  ordwe  4674  wessep  4676  peano2  4693  finds  4698  finds2  4699  relss  4813  ssrel  4814  ssrel2  4816  ssrelrel  4826  xpsspw  4838  relop  4880  cnvss  4903  dmss  4930  dmcosseq  5004  funss  5345  imadif  5410  imain  5412  fss  5494  fun  5508  brprcneu  5632  isores3  5956  isopolem  5963  isosolem  5965  tposfn2  6432  tposfo2  6433  tposf1o2  6436  smores  6458  tfr1onlemaccex  6514  tfrcllemaccex  6527  iinerm  6776  xpdom2  7015  ssenen  7037  exmidpw  7100  exmidpweq  7101  nnnninfeq2  7328  recexprlemlol  7846  recexprlemupu  7848  axpre-ltwlin  8103  axpre-apti  8105  nnindnn  8113  nnind  9159  uzind  9591  hashfacen  11101  pfxccatin12lem2  11316  cau3lem  11692  tgcl  14807  epttop  14833  txcnp  15014  plycj  15504  gausslemma2dlem0i  15805  gausslemma2dlem1a  15806  nnnninfex  16675