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  2061  moimv  2063  2euswapdc  2088  nelcon3d  2412  ralim  2489  ralimdaa  2496  ralimdv2  2500  rexim  2524  reximdv2  2529  rmoim  2880  ssel  3086  sstr2  3099  ssrexf  3154  ssrmof  3155  sscon  3205  ssdif  3206  unss1  3240  ssrin  3296  prel12  3693  uniss  3752  ssuni  3753  intss  3787  intssunim  3788  iunss1  3819  iinss1  3820  ss2iun  3823  disjss2  3904  disjss1  3907  ssbrd  3966  sspwb  4133  poss  4215  pofun  4229  soss  4231  sess1  4254  sess2  4255  ordwe  4485  wessep  4487  peano2  4504  finds  4509  finds2  4510  relss  4621  ssrel  4622  ssrel2  4624  ssrelrel  4634  xpsspw  4646  relop  4684  cnvss  4707  dmss  4733  dmcosseq  4805  funss  5137  imadif  5198  imain  5200  fss  5279  fun  5290  brprcneu  5407  isores3  5709  isopolem  5716  isosolem  5718  tposfn2  6156  tposfo2  6157  tposf1o2  6160  smores  6182  tfr1onlemaccex  6238  tfrcllemaccex  6251  iinerm  6494  xpdom2  6718  ssenen  6738  exmidpw  6795  recexprlemlol  7427  recexprlemupu  7429  axpre-ltwlin  7684  axpre-apti  7686  nnindnn  7694  nnind  8729  uzind  9155  hashfacen  10572  cau3lem  10879  tgcl  12222  epttop  12248  txcnp  12429