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	biimtrid 244	. 2 ⊢ (𝜑 → (𝜃 → 𝜒))
4		3imtr4g.3	. 2 ⊢ (𝜏 ↔ 𝜒)
5	3, 4	imbitrrdi 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  1452  3orim123d  1453  sbi1  2083  moim  2550  mo3  2570  2euswapv  2636  2euswap  2651  exists2  2667  nelcon3d  3044  ral2imi  3080  ralimdv2  3150  reximdv2  3151  reximd2a  3251  moeq3  3655  rmoim  3683  2reuswap  3689  2reuswap2  3690  2rmoswap  3704  ssel  3911  ssrexf  3984  ssrmof  3985  ssralv  3986  ssrexv  3987  ss2abim  3994  ss2abdv  3999  rabss3d  4015  sscon  4076  ssdif  4077  unss1  4117  ssrin  4173  difin0ss  4304  r19.2z  4430  sspw  4543  uniss  4849  ssuni  4866  intssuni  4903  iinssiun  4938  iunss1  4939  iinss1  4940  ss2iun  4943  iunxdif3  5027  disjss2  5045  disjss1  5048  disjss3  5074  ssbrd  5118  poss  5531  pofun  5547  soss  5549  frss  5585  sess1  5586  sess2  5587  wess  5607  relss  5728  ssrel2  5731  ssrelrel  5742  relop  5795  dmss  5851  dmcosseq  5927  dmcosseqOLD  5928  dmcosseqOLDOLD  5929  funss  6508  f1imadifssran  6575  fss  6675  fun  6693  brprcneu  6821  brprcneuALT  6822  f1eqcocnv  7249  isores3  7283  isomin  7285  isopolem  7293  isosolem  7295  isowe2  7298  ovmpos  7508  dfwe2  7721  epweon  7722  onint  7737  orduniorsuc  7774  trom  7819  finds  7840  finds2  7842  f1oweALT  7918  tposfn2  8192  tposfo2  8193  tposf1o2  8196  fprlem2  8245  smores  8286  tz7.48lem  8374  tz7.48-3  8377  oaass  8490  brinxper  8667  iiner  8730  xpdom2  9004  ssenen  9083  pssnn  9097  hartogs  9453  card2on  9463  ackbij1  10154  cfub  10166  fin23lem27  10245  fin1a2lem11  10327  fin1a2lem13  10329  hsmexlem2  10344  zorn2lem4  10416  ondomon  10480  gchina  10617  intgru  10732  ingru  10733  addclprlem2  10935  psslinpr  10949  ltexprlem3  10956  ltexprlem4  10957  reclem2pr  10966  suplem1pr  10970  sup2  12107  nnind  12187  nnunb  12428  uzind  12616  xmullem2  13212  xrsupsslem  13254  xrinfmsslem  13255  seqof  14016  hashfacen  14411  sswrd  14479  wrdind  14679  wrd2ind  14680  pfxccatin12lem2  14688  cau3lem  15312  caubnd  15316  sumodd  16352  vdwnnlem2  16962  ramub2  16980  fthres2  17896  oduprs  18261  odupos  18287  chnrss  18576  chndss  18577  cycsubm  19172  lsmdisj2  19652  gsumxp2  19950  pgpfac1lem3  20049  nrhmzr  20513  subrgdvds  20562  lspdisj  21122  lspprat  21150  lbsextlem2  21156  ocv2ss  21652  ocvin  21653  coe1fzgsumd  22294  evl1gsumd  22347  tgcl  22956  epttop  22996  cmpsub  23387  tgcmp  23388  hauscmplem  23393  dfconn2  23406  llyss  23466  nllyss  23467  locfincmp  23513  txcnpi  23595  txcnp  23607  snfil  23851  fgcl  23865  filconn  23870  filuni  23872  cfinfil  23880  csdfil  23881  supfil  23882  ufildom1  23913  fin1aufil  23919  fmfnfmlem3  23943  ptcmplem2  24040  cldsubg  24098  iscau3  25267  iscau4  25268  caussi  25286  volfiniun  25536  plycj  26264  plycjOLD  26266  abelth  26428  wilthlem2  27054  lgsdir2lem4  27313  gausslemma2dlem0i  27349  gausslemma2dlem1a  27350  pntleml  27596  ltsres  27648  nosupno  27689  noinfno  27704  noseqinds  28307  uhgr0vsize0  29330  cusgrfilem2  29547  uhgrvd00  29625  clwwisshclwws  30107  frcond3  30361  frgrncvvdeqlem2  30392  lpni  30573  ubthlem1  30963  chintcli  31424  h1de2i  31646  spansnm0i  31743  strlem1  32343  mdslmd1i  32422  reuxfrdf  32582  n0nsnel  32607  disjss1f  32665  disjpreima  32677  ssrelf  32711  suppss3  32819  nnindf  32916  wrdt2ind  33036  crefss  34045  esumpcvgval  34274  cbvex1v  35271  r1filim  35300  onvf1odlem4  35349  subgrtrl  35376  subgrpth  35377  subgrcycl  35378  derangenlem  35414  connpconn  35478  cvmsss2  35517  pocnv  36006  wzel  36065  in-ax8  36467  naim1  36632  naim2  36633  waj-ax  36657  lukshef-ax2  36658  ttctr  36736  dfttc2g  36749  bj-exim  36965  bj-sbievw1  37213  wl-dfcleq  37891  poimirlem26  38028  poimirlem30  38032  poimirlem32  38034  itg2addnclem  38053  ismtybndlem  38188  ablo4pnp  38262  isdrngo3  38341  keridl  38414  ispridl2  38420  ispridlc  38452  trcoss  38954  funALTVss  39166  disjss  39213  eldisjss  39220  prter1  39386  lshpdisj  39494  snatpsubN  40257  pmapglb2N  40278  pmapglb2xN  40279  elpaddn0  40307  sn-sup2  42996  nna4b4nsq  43125  mzpindd  43210  pellexlem3  43291  pellexlem5  43293  pellex  43295  2nn0ind  43405  lnr2i  43576  ofoaid1  43818  ofoaid2  43819  intabssd  43978  iunrelexpuztr  44178  hess  44239  frege52aid  44317  frege52b  44348  neik0pk1imk0  44506  relpmin  45411  rankrelp  45419  n0nsn2el  47502  imasetpreimafvbijlemfv1  47892  isubgredg  48371  stgrusgra  48464  isubgr3stgrlem6  48476  iinfsubc  49562  elsetrecslem  50203