Theorem 3imtr4g 284

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

Syntax hints:   → wi 4   ↔ wb 195

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 196

This theorem is referenced by:  3anim123d  1398  3orim123d  1399  mo3  2495  moim  2507  2euswap  2536  nelcon3d  2895  ral2imi  2931  ralimdv2  2944  rexim  2991  reximd2a  2996  reximdv2  2997  moeq3  3350  rmoim  3374  2reuswap  3377  ssel  3562  sstr2  3575  ssrexf  3628  sscon  3706  ssdif  3707  unss1  3744  ssrin  3800  difin0ss  3900  r19.2z  4012  prel12  4323  uniss  4394  ssuni  4395  ssuniOLD  4396  intssuni  4434  iunss1  4468  iinss1  4469  ss2iun  4472  iunxdif3  4542  disjss2  4556  disjss1  4559  disjss3  4582  ssbrd  4626  sspwb  4844  poss  4961  pofun  4975  soss  4977  frss  5005  sess1  5006  sess2  5007  wess  5025  relss  5129  ssrelOLD  5131  ssrel2  5133  ssrelrel  5143  relop  5194  cnvssOLD  5217  dmss  5245  dmcosseq  5308  funss  5822  fss  5969  fun  5979  brprcneu  6096  f1eqcocnv  6456  isores3  6485  isomin  6487  isopolem  6495  isosolem  6497  isowe2  6500  ovmpt2s  6682  dfwe2  6873  onint  6887  orduniorsuc  6922  ordom  6966  finds  6984  finds2  6986  f1oweALT  7043  tposfn2  7261  tposfo2  7262  tposf1o2  7265  smores  7336  tz7.48lem  7423  tz7.48-3  7426  oaass  7528  iiner  7706  xpdom2  7940  ssenen  8019  pssnn  8063  hartogs  8332  card2on  8342  ackbij1  8943  cfub  8954  fin23lem27  9033  fin1a2lem11  9115  fin1a2lem13  9117  hsmexlem2  9132  zorn2lem4  9204  ondomon  9264  gchina  9400  intgru  9515  ingru  9516  addclprlem2  9718  psslinpr  9732  ltexprlem3  9739  ltexprlem4  9740  reclem2pr  9749  suplem1pr  9753  sup2  10858  nnind  10915  nnunb  11165  uzind  11345  xmullem2  11967  xrsupsslem  12009  xrinfmsslem  12010  seqof  12720  hashfacen  13095  sswrd  13168  wrdind  13328  wrd2ind  13329  swrdccatin12lem2  13340  cau3lem  13942  caubnd  13946  sumodd  14949  vdwnnlem2  15538  ramub2  15556  setsstruct  15727  fthres2  16415  odupos  16958  lsmdisj2  17918  pgpfac1lem3  18299  subrgdvds  18617  lspdisj  18946  lspprat  18974  lbsextlem2  18980  coe1fzgsumd  19493  evl1gsumd  19542  ocv2ss  19836  ocvin  19837  tgcl  20584  epttop  20623  cmpsub  21013  tgcmp  21014  hauscmplem  21019  dfcon2  21032  llyss  21092  nllyss  21093  locfincmp  21139  txcnpi  21221  txcnp  21233  snfil  21478  fgcl  21492  filcon  21497  filuni  21499  cfinfil  21507  csdfil  21508  supfil  21509  ufildom1  21540  fin1aufil  21546  fmfnfmlem3  21570  ptcmplem2  21667  cldsubg  21724  iscau3  22884  iscau4  22885  caussi  22903  volfiniun  23122  plycj  23837  abelth  23999  wilthlem2  24595  lgsdir2lem4  24853  gausslemma2dlem0i  24889  gausslemma2dlem1a  24890  pntleml  25100  cusgrafilem2  26008  frisusgranb  26524  frgrancvvdeqlem3  26559  lpni  26722  ubthlem1  27110  chintcli  27574  h1de2i  27796  spansnm0i  27893  strlem1  28493  mdslmd1i  28572  2reuswap2  28712  ssrmo  28718  rabss3d  28736  disjss1f  28768  disjpreima  28779  ssrelf  28805  suppss3  28890  nnindf  28952  oduprs  28987  crefss  29244  esumpcvgval  29467  derangenlem  30407  conpcon  30471  cvmsss2  30510  pocnv  30907  wzel  31015  wzelOLD  31016  sltres  31061  nocvxmin  31090  naim1  31554  naim2  31555  waj-ax  31583  lukshef-ax2  31584  bj-ssbim  31810  bj-mo3OLD  32022  poimirlem26  32605  poimirlem30  32609  poimirlem32  32611  itg2addnclem  32631  ismtybndlem  32775  ablo4pnp  32849  isdrngo3  32928  keridl  33001  ispridl2  33007  ispridlc  33039  prter1  33182  lshpdisj  33292  snatpsubN  34054  pmapglb2N  34075  pmapglb2xN  34076  elpaddn0  34104  mzpindd  36327  pellexlem3  36413  pellexlem5  36415  pellex  36417  2nn0ind  36528  lnr2i  36705  intabssd  36935  iunrelexpuztr  37030  hess  37094  frege52aid  37172  frege52b  37203  neik0pk1imk0  37365  2rmoswap  39833  pfxccatin12lem2  40287  uhgr0vsize0  40465  cusgrfilem2  40672  uhgrvd00  40750  clwwisshclwws  41235  frcond3  41440  frgrncvvdeqlem3  41471  nrhmzr  41663  elsetrecslem  42243