Theorem 3imtr4g 285

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

Syntax hints:   → wi 4   ↔ wb 196

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 197

This theorem is referenced by:  3anim123d  1406  3orim123d  1407  mo3  2507  moim  2519  2euswap  2548  nelcon3d  2909  ral2imi  2947  ralimdv2  2961  rexim  3008  reximd2a  3013  reximdv2  3014  moeq3  3383  rmoim  3407  2reuswap  3410  ssel  3597  sstr2  3610  ssrexf  3665  sscon  3744  ssdif  3745  unss1  3782  ssrin  3838  difin0ss  3946  r19.2z  4060  prel12  4383  uniss  4458  ssuni  4459  ssuniOLD  4460  intssuni  4499  iunss1  4532  iinss1  4533  ss2iun  4536  iunxdif3  4606  disjss2  4623  disjss1  4626  disjss3  4652  ssbrd  4696  sspwb  4917  poss  5037  pofun  5051  soss  5053  frss  5081  sess1  5082  sess2  5083  wess  5101  relss  5206  ssrelOLD  5208  ssrel2  5210  ssrelrel  5220  relop  5272  cnvssOLD  5295  dmss  5323  dmcosseq  5387  funss  5907  fss  6056  fun  6066  brprcneu  6184  f1eqcocnv  6556  isores3  6585  isomin  6587  isopolem  6595  isosolem  6597  isowe2  6600  ovmpt2s  6784  dfwe2  6981  onint  6995  orduniorsuc  7030  ordom  7074  finds  7092  finds2  7094  f1oweALT  7152  tposfn2  7374  tposfo2  7375  tposf1o2  7378  smores  7449  tz7.48lem  7536  tz7.48-3  7539  oaass  7641  iiner  7819  xpdom2  8055  ssenen  8134  pssnn  8178  hartogs  8449  card2on  8459  ackbij1  9060  cfub  9071  fin23lem27  9150  fin1a2lem11  9232  fin1a2lem13  9234  hsmexlem2  9249  zorn2lem4  9321  ondomon  9385  gchina  9521  intgru  9636  ingru  9637  addclprlem2  9839  psslinpr  9853  ltexprlem3  9860  ltexprlem4  9861  reclem2pr  9870  suplem1pr  9874  sup2  10979  nnind  11038  nnunb  11288  uzind  11469  xmullem2  12095  xrsupsslem  12137  xrinfmsslem  12138  seqof  12858  hashfacen  13238  sswrd  13313  wrdind  13476  wrd2ind  13477  swrdccatin12lem2  13489  cau3lem  14094  caubnd  14098  sumodd  15111  vdwnnlem2  15700  ramub2  15718  setsstructOLD  15899  fthres2  16592  odupos  17135  lsmdisj2  18095  pgpfac1lem3  18476  subrgdvds  18794  lspdisj  19125  lspprat  19153  lbsextlem2  19159  coe1fzgsumd  19672  evl1gsumd  19721  ocv2ss  20017  ocvin  20018  tgcl  20773  epttop  20813  cmpsub  21203  tgcmp  21204  hauscmplem  21209  dfconn2  21222  llyss  21282  nllyss  21283  locfincmp  21329  txcnpi  21411  txcnp  21423  snfil  21668  fgcl  21682  filconn  21687  filuni  21689  cfinfil  21697  csdfil  21698  supfil  21699  ufildom1  21730  fin1aufil  21736  fmfnfmlem3  21760  ptcmplem2  21857  cldsubg  21914  iscau3  23076  iscau4  23077  caussi  23095  volfiniun  23315  plycj  24033  abelth  24195  wilthlem2  24795  lgsdir2lem4  25053  gausslemma2dlem0i  25089  gausslemma2dlem1a  25090  pntleml  25300  uhgr0vsize0  26131  cusgrfilem2  26352  uhgrvd00  26430  clwwisshclwws  26928  frcond3  27133  frgrncvvdeqlem2  27164  lpni  27332  ubthlem1  27726  chintcli  28190  h1de2i  28412  spansnm0i  28509  strlem1  29109  mdslmd1i  29188  2reuswap2  29328  ssrmo  29334  rabss3d  29351  iinssiun  29377  disjss1f  29386  disjpreima  29397  ssrelf  29425  suppss3  29502  nnindf  29565  oduprs  29656  crefss  29916  esumpcvgval  30140  derangenlem  31153  connpconn  31217  cvmsss2  31256  pocnv  31653  wzel  31771  wzelOLD  31772  sltres  31815  nosupno  31849  nocvxmin  31894  naim1  32384  naim2  32385  waj-ax  32413  lukshef-ax2  32414  bj-ssbim  32621  bj-mo3OLD  32832  poimirlem26  33435  poimirlem30  33439  poimirlem32  33441  itg2addnclem  33461  ismtybndlem  33605  ablo4pnp  33679  isdrngo3  33758  keridl  33831  ispridl2  33837  ispridlc  33869  ssbr  34008  prter1  34164  lshpdisj  34274  snatpsubN  35036  pmapglb2N  35057  pmapglb2xN  35058  elpaddn0  35086  mzpindd  37309  pellexlem3  37395  pellexlem5  37397  pellex  37399  2nn0ind  37510  lnr2i  37686  intabssd  37916  iunrelexpuztr  38011  hess  38074  frege52aid  38152  frege52b  38183  neik0pk1imk0  38345  2rmoswap  41184  pfxccatin12lem2  41424  nrhmzr  41873  elsetrecslem  42444