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  1253  3orim123d  1254  hbbid  1510  spsbim  1768  moim  2009  moimv  2011  2euswapdc  2036  ralim  2430  ralimdaa  2436  ralimdv2  2439  rexim  2463  reximdv2  2468  rmoim  2805  ssel  3008  sstr2  3021  sscon  3123  ssdif  3124  unss1  3158  ssrin  3214  prel12  3598  uniss  3657  ssuni  3658  intss  3692  intssunim  3693  iunss1  3724  iinss1  3725  ss2iun  3728  disjss2  3804  disjss1  3807  ssbrd  3861  sspwb  4017  poss  4099  pofun  4113  soss  4115  sess1  4138  sess2  4139  ordwe  4364  wessep  4366  peano2  4383  finds  4388  finds2  4389  relss  4493  ssrel  4494  ssrel2  4496  ssrelrel  4506  xpsspw  4518  relop  4554  cnvss  4577  dmss  4603  dmcosseq  4672  funss  4999  imadif  5059  imain  5061  fss  5136  fun  5147  brprcneu  5261  isores3  5555  isopolem  5562  isosolem  5564  tposfn2  5985  tposfo2  5986  tposf1o2  5989  smores  6011  tfr1onlemaccex  6067  tfrcllemaccex  6080  iinerm  6316  xpdom2  6499  ssenen  6519  exmidpw  6576  recexprlemlol  7129  recexprlemupu  7131  axpre-ltwlin  7362  axpre-apti  7364  nnindnn  7372  nnind  8373  uzind  8790  hashfacen  10137  cau3lem  10442