Theorem 3imtr4g 296

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  3anim123d  1444  3orim123d  1445  sbi1  2070  moim  2542  mo3  2562  2euswapv  2628  2euswap  2643  exists2  2660  nelcon3d  3039  ral2imi  3074  ralimdv2  3150  reximdv2  3151  reximd2a  3256  moeq3  3702  rmoim  3730  2reuswap  3736  2reuswap2  3737  2rmoswap  3751  ssel  3959  sstr2OLD  3973  ssrexf  4032  ssrmof  4033  ssralv  4034  ssrexv  4035  ss2abdv  4048  rabss3d  4063  sscon  4125  ssdif  4126  unss1  4167  ssrin  4224  difin0ss  4355  r19.2z  4477  sspw  4593  uniss  4897  ssuni  4914  intssuni  4952  iinssiun  4987  iunss1  4988  iinss1  4989  ss2iun  4992  iunxdif3  5077  disjss2  5095  disjss1  5098  disjss3  5124  ssbrd  5168  poss  5576  pofun  5592  soss  5594  frss  5631  sess1  5632  sess2  5633  wess  5653  relss  5773  ssrel2  5777  ssrelrel  5788  relop  5843  dmss  5895  dmcosseq  5969  dmcosseqOLD  5970  funss  6566  f1imadifssran  6633  fss  6733  fun  6751  brprcneu  6877  brprcneuALT  6878  f1eqcocnv  7304  isores3  7338  isomin  7340  isopolem  7348  isosolem  7350  isowe2  7353  ovmpos  7564  dfwe2  7777  epweon  7778  onint  7793  orduniorsuc  7833  trom  7879  finds  7901  finds2  7903  f1oweALT  7980  tposfn2  8256  tposfo2  8257  tposf1o2  8260  fprlem2  8309  smores  8375  tz7.48lem  8464  tz7.48-3  8467  oaass  8582  brinxper  8757  iiner  8812  xpdom2  9090  ssenen  9174  pssnn  9191  hartogs  9567  card2on  9577  ackbij1  10260  cfub  10272  fin23lem27  10351  fin1a2lem11  10433  fin1a2lem13  10435  hsmexlem2  10450  zorn2lem4  10522  ondomon  10586  gchina  10722  intgru  10837  ingru  10838  addclprlem2  11040  psslinpr  11054  ltexprlem3  11061  ltexprlem4  11062  reclem2pr  11071  suplem1pr  11075  sup2  12207  nnind  12267  nnunb  12506  uzind  12694  xmullem2  13290  xrsupsslem  13332  xrinfmsslem  13333  seqof  14083  hashfacen  14476  sswrd  14543  wrdind  14743  wrd2ind  14744  pfxccatin12lem2  14752  cau3lem  15376  caubnd  15380  sumodd  16408  vdwnnlem2  17017  ramub2  17035  fthres2  17955  oduprs  18321  odupos  18347  cycsubm  19194  lsmdisj2  19673  gsumxp2  19971  pgpfac1lem3  20070  nrhmzr  20510  subrgdvds  20559  lspdisj  21100  lspprat  21128  lbsextlem2  21134  ocv2ss  21658  ocvin  21659  coe1fzgsumd  22275  evl1gsumd  22328  tgcl  22942  epttop  22982  cmpsub  23373  tgcmp  23374  hauscmplem  23379  dfconn2  23392  llyss  23452  nllyss  23453  locfincmp  23499  txcnpi  23581  txcnp  23593  snfil  23837  fgcl  23851  filconn  23856  filuni  23858  cfinfil  23866  csdfil  23867  supfil  23868  ufildom1  23899  fin1aufil  23905  fmfnfmlem3  23929  ptcmplem2  24026  cldsubg  24084  iscau3  25267  iscau4  25268  caussi  25286  volfiniun  25537  plycj  26272  plycjOLD  26274  abelth  26440  wilthlem2  27067  lgsdir2lem4  27327  gausslemma2dlem0i  27363  gausslemma2dlem1a  27364  pntleml  27610  sltres  27662  nosupno  27703  noinfno  27718  nocvxmin  27778  noseqinds  28254  uhgr0vsize0  29203  cusgrfilem2  29421  uhgrvd00  29499  clwwisshclwws  29981  frcond3  30235  frgrncvvdeqlem2  30266  lpni  30446  ubthlem1  30836  chintcli  31297  h1de2i  31519  spansnm0i  31616  strlem1  32216  mdslmd1i  32295  reuxfrdf  32457  n0nsnel  32481  disjss1f  32532  disjpreima  32544  ssrelf  32574  suppss3  32682  nnindf  32768  wrdt2ind  32885  crefss  33789  esumpcvgval  34020  cbvex1v  35029  subgrtrl  35079  subgrpth  35080  subgrcycl  35081  derangenlem  35117  connpconn  35181  cvmsss2  35220  pocnv  35704  wzel  35766  in-ax8  36166  naim1  36331  naim2  36332  waj-ax  36356  lukshef-ax2  36357  bj-eximALT  36583  bj-sbievw1  36787  poimirlem26  37594  poimirlem30  37598  poimirlem32  37600  itg2addnclem  37619  ismtybndlem  37754  ablo4pnp  37828  isdrngo3  37907  keridl  37980  ispridl2  37986  ispridlc  38018  trcoss  38424  funALTVss  38641  disjss  38673  eldisjss  38680  prter1  38821  lshpdisj  38929  snatpsubN  39693  pmapglb2N  39714  pmapglb2xN  39715  elpaddn0  39743  ss2ab1  42199  sn-sup2  42446  nna4b4nsq  42615  mzpindd  42702  pellexlem3  42787  pellexlem5  42789  pellex  42791  2nn0ind  42902  lnr2i  43073  ofoaid1  43316  ofoaid2  43317  intabssd  43477  iunrelexpuztr  43677  hess  43738  frege52aid  43816  frege52b  43847  neik0pk1imk0  44005  relpmin  44918  rankrelp  44922  n0nsn2el  46983  imasetpreimafvbijlemfv1  47336  isubgredg  47798  stgrusgra  47872  isubgr3stgrlem6  47884  elsetrecslem  49214