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  3255  moeq3  3700  rmoim  3728  2reuswap  3734  2reuswap2  3735  2rmoswap  3749  ssel  3957  sstr2OLD  3971  ssrexf  4030  ssrmof  4031  ssralv  4032  ssrexv  4033  ss2abdv  4046  rabss3d  4061  sscon  4123  ssdif  4124  unss1  4165  ssrin  4222  difin0ss  4353  r19.2z  4475  sspw  4591  uniss  4895  ssuni  4912  intssuni  4950  iinssiun  4985  iunss1  4986  iinss1  4987  ss2iun  4990  iunxdif3  5075  disjss2  5093  disjss1  5096  disjss3  5122  ssbrd  5166  poss  5574  pofun  5590  soss  5592  frss  5629  sess1  5630  sess2  5631  wess  5651  relss  5771  ssrel2  5775  ssrelrel  5786  relop  5841  dmss  5893  dmcosseq  5967  dmcosseqOLD  5968  funss  6565  f1imadifssran  6632  fss  6732  fun  6750  brprcneu  6876  brprcneuALT  6877  f1eqcocnv  7303  isores3  7337  isomin  7339  isopolem  7347  isosolem  7349  isowe2  7352  ovmpos  7563  dfwe2  7776  epweon  7777  onint  7792  orduniorsuc  7832  trom  7878  finds  7900  finds2  7902  f1oweALT  7979  tposfn2  8255  tposfo2  8256  tposf1o2  8259  fprlem2  8308  smores  8374  tz7.48lem  8463  tz7.48-3  8466  oaass  8581  brinxper  8756  iiner  8811  xpdom2  9089  ssenen  9173  pssnn  9190  hartogs  9566  card2on  9576  ackbij1  10259  cfub  10271  fin23lem27  10350  fin1a2lem11  10432  fin1a2lem13  10434  hsmexlem2  10449  zorn2lem4  10521  ondomon  10585  gchina  10721  intgru  10836  ingru  10837  addclprlem2  11039  psslinpr  11053  ltexprlem3  11060  ltexprlem4  11061  reclem2pr  11070  suplem1pr  11074  sup2  12206  nnind  12266  nnunb  12505  uzind  12693  xmullem2  13289  xrsupsslem  13331  xrinfmsslem  13332  seqof  14082  hashfacen  14476  sswrd  14543  wrdind  14743  wrd2ind  14744  pfxccatin12lem2  14752  cau3lem  15376  caubnd  15380  sumodd  16408  vdwnnlem2  17017  ramub2  17035  fthres2  17951  oduprs  18317  odupos  18343  cycsubm  19190  lsmdisj2  19669  gsumxp2  19967  pgpfac1lem3  20066  nrhmzr  20506  subrgdvds  20555  lspdisj  21096  lspprat  21124  lbsextlem2  21130  ocv2ss  21646  ocvin  21647  coe1fzgsumd  22257  evl1gsumd  22310  tgcl  22924  epttop  22964  cmpsub  23355  tgcmp  23356  hauscmplem  23361  dfconn2  23374  llyss  23434  nllyss  23435  locfincmp  23481  txcnpi  23563  txcnp  23575  snfil  23819  fgcl  23833  filconn  23838  filuni  23840  cfinfil  23848  csdfil  23849  supfil  23850  ufildom1  23881  fin1aufil  23887  fmfnfmlem3  23911  ptcmplem2  24008  cldsubg  24066  iscau3  25249  iscau4  25250  caussi  25268  volfiniun  25519  plycj  26254  plycjOLD  26256  abelth  26422  wilthlem2  27049  lgsdir2lem4  27309  gausslemma2dlem0i  27345  gausslemma2dlem1a  27346  pntleml  27592  sltres  27644  nosupno  27685  noinfno  27700  nocvxmin  27760  noseqinds  28236  uhgr0vsize0  29185  cusgrfilem2  29403  uhgrvd00  29481  clwwisshclwws  29963  frcond3  30217  frgrncvvdeqlem2  30248  lpni  30428  ubthlem1  30818  chintcli  31279  h1de2i  31501  spansnm0i  31598  strlem1  32198  mdslmd1i  32277  reuxfrdf  32439  n0nsnel  32463  disjss1f  32521  disjpreima  32533  ssrelf  32563  suppss3  32671  nnindf  32766  wrdt2ind  32883  crefss  33823  esumpcvgval  34054  cbvex1v  35063  subgrtrl  35113  subgrpth  35114  subgrcycl  35115  derangenlem  35151  connpconn  35215  cvmsss2  35254  pocnv  35738  wzel  35800  in-ax8  36200  naim1  36365  naim2  36366  waj-ax  36390  lukshef-ax2  36391  bj-eximALT  36617  bj-sbievw1  36821  poimirlem26  37628  poimirlem30  37632  poimirlem32  37634  itg2addnclem  37653  ismtybndlem  37788  ablo4pnp  37862  isdrngo3  37941  keridl  38014  ispridl2  38020  ispridlc  38052  trcoss  38458  funALTVss  38675  disjss  38707  eldisjss  38714  prter1  38855  lshpdisj  38963  snatpsubN  39727  pmapglb2N  39748  pmapglb2xN  39749  elpaddn0  39777  ss2ab1  42233  sn-sup2  42480  nna4b4nsq  42649  mzpindd  42735  pellexlem3  42820  pellexlem5  42822  pellex  42824  2nn0ind  42935  lnr2i  43106  ofoaid1  43348  ofoaid2  43349  intabssd  43509  iunrelexpuztr  43709  hess  43770  frege52aid  43848  frege52b  43879  neik0pk1imk0  44037  relpmin  44945  rankrelp  44949  n0nsn2el  47010  imasetpreimafvbijlemfv1  47363  isubgredg  47825  stgrusgra  47899  isubgr3stgrlem6  47911  iinfsubc  48931  elsetrecslem  49313