Theorem 3imtr4g 298

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  3anim123d  1439  3orim123d  1440  sbi1  2072  sbequivvOLD  2330  sbimdvOLD  2512  sbimdOLD  2514  moim  2622  mo3  2644  2euswapv  2711  2euswap  2726  exists2  2745  nelcon3d  3135  ral2imi  3156  ralimdv2  3176  rexim  3241  reximdv2  3271  reximd2a  3312  moeq3  3702  rmoim  3730  2reuswap  3736  2reuswap2  3737  2rmoswap  3751  ssel  3960  sstr2  3973  ssrexf  4030  ssrmof  4031  sscon  4114  ssdif  4115  unss1  4154  ssrin  4209  difin0ss  4327  r19.2z  4439  uniss  4852  ssuni  4853  intssuni  4890  iinssiun  4924  iunss1  4925  iinss1  4926  ss2iun  4929  iunxdif3  5009  disjss2  5026  disjss1  5029  disjss3  5057  ssbrd  5101  sspwb  5333  poss  5470  pofun  5485  soss  5487  frss  5516  sess1  5517  sess2  5518  wess  5536  relss  5650  ssrel2  5653  ssrelrel  5663  relop  5715  dmss  5765  dmcosseq  5838  funss  6368  fss  6521  fun  6534  brprcneu  6656  f1eqcocnv  7051  isores3  7082  isomin  7084  isopolem  7092  isosolem  7094  isowe2  7097  ovmpos  7292  dfwe2  7490  onint  7504  orduniorsuc  7539  ordom  7583  finds  7602  finds2  7604  f1oweALT  7667  tposfn2  7908  tposfo2  7909  tposf1o2  7912  smores  7983  tz7.48lem  8071  tz7.48-3  8074  oaass  8181  iiner  8363  xpdom2  8606  ssenen  8685  pssnn  8730  hartogs  9002  card2on  9012  ackbij1  9654  cfub  9665  fin23lem27  9744  fin1a2lem11  9826  fin1a2lem13  9828  hsmexlem2  9843  zorn2lem4  9915  ondomon  9979  gchina  10115  intgru  10230  ingru  10231  addclprlem2  10433  psslinpr  10447  ltexprlem3  10454  ltexprlem4  10455  reclem2pr  10464  suplem1pr  10468  sup2  11591  nnind  11650  nnunb  11887  uzind  12068  xmullem2  12652  xrsupsslem  12694  xrinfmsslem  12695  seqof  13421  hashfacen  13806  sswrd  13863  wrdind  14078  wrd2ind  14079  pfxccatin12lem2  14087  cau3lem  14708  caubnd  14712  sumodd  15733  vdwnnlem2  16326  ramub2  16344  fthres2  17196  odupos  17739  cycsubm  18339  lsmdisj2  18802  gsumxp2  19094  pgpfac1lem3  19193  subrgdvds  19543  lspdisj  19891  lspprat  19919  lbsextlem2  19925  coe1fzgsumd  20464  evl1gsumd  20514  ocv2ss  20811  ocvin  20812  tgcl  21571  epttop  21611  cmpsub  22002  tgcmp  22003  hauscmplem  22008  dfconn2  22021  llyss  22081  nllyss  22082  locfincmp  22128  txcnpi  22210  txcnp  22222  snfil  22466  fgcl  22480  filconn  22485  filuni  22487  cfinfil  22495  csdfil  22496  supfil  22497  ufildom1  22528  fin1aufil  22534  fmfnfmlem3  22558  ptcmplem2  22655  cldsubg  22713  iscau3  23875  iscau4  23876  caussi  23894  volfiniun  24142  plycj  24861  abelth  25023  wilthlem2  25640  lgsdir2lem4  25898  gausslemma2dlem0i  25934  gausslemma2dlem1a  25935  pntleml  26181  uhgr0vsize0  27015  cusgrfilem2  27232  uhgrvd00  27310  clwwisshclwws  27787  frcond3  28042  frgrncvvdeqlem2  28073  lpni  28251  ubthlem1  28641  chintcli  29102  h1de2i  29324  spansnm0i  29421  strlem1  30021  mdslmd1i  30100  reuxfrdf  30249  rabss3d  30270  disjss1f  30316  disjpreima  30328  ssrelf  30360  suppss3  30454  nnindf  30529  wrdt2ind  30622  oduprs  30638  crefss  31108  esumpcvgval  31332  subgrtrl  32375  subgrpth  32376  subgrcycl  32377  derangenlem  32413  connpconn  32477  cvmsss2  32516  pocnv  32994  wzel  33106  fprlem2  33133  sltres  33164  nosupno  33198  nocvxmin  33243  naim1  33732  naim2  33733  waj-ax  33757  lukshef-ax2  33758  bj-eximALT  33969  bj-sbievw1  34164  poimirlem26  34912  poimirlem30  34916  poimirlem32  34918  itg2addnclem  34937  ismtybndlem  35078  ablo4pnp  35152  isdrngo3  35231  keridl  35304  ispridl2  35310  ispridlc  35342  trcoss  35716  funALTVss  35926  disjss  35958  eldisjss  35965  prter1  36009  lshpdisj  36117  snatpsubN  36880  pmapglb2N  36901  pmapglb2xN  36902  elpaddn0  36930  mzpindd  39336  pellexlem3  39421  pellexlem5  39423  pellex  39425  2nn0ind  39535  lnr2i  39709  intabssd  39878  iunrelexpuztr  40057  hess  40119  frege52aid  40197  frege52b  40228  neik0pk1imk0  40390  imasetpreimafvbijlemfv1  43557  ichan  43624  nrhmzr  44138  elsetrecslem  44795