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  1445  3orim123d  1446  sbi1  2072  moim  2544  mo3  2564  2euswapv  2630  2euswap  2645  exists2  2662  nelcon3d  3041  ral2imi  3076  ralimdv2  3150  reximdv2  3151  reximd2a  3256  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  4896  ssuni  4913  intssuni  4951  iinssiun  4986  iunss1  4987  iinss1  4988  ss2iun  4991  iunxdif3  5076  disjss2  5094  disjss1  5097  disjss3  5123  ssbrd  5167  poss  5568  pofun  5584  soss  5586  frss  5623  sess1  5624  sess2  5625  wess  5645  relss  5765  ssrel2  5769  ssrelrel  5780  relop  5835  dmss  5887  dmcosseq  5961  dmcosseqOLD  5962  funss  6560  f1imadifssran  6627  fss  6727  fun  6745  brprcneu  6871  brprcneuALT  6872  f1eqcocnv  7299  isores3  7333  isomin  7335  isopolem  7343  isosolem  7345  isowe2  7348  ovmpos  7560  dfwe2  7773  epweon  7774  onint  7789  orduniorsuc  7829  trom  7875  finds  7897  finds2  7899  f1oweALT  7976  tposfn2  8252  tposfo2  8253  tposf1o2  8256  fprlem2  8305  smores  8371  tz7.48lem  8460  tz7.48-3  8463  oaass  8578  brinxper  8753  iiner  8808  xpdom2  9086  ssenen  9170  pssnn  9187  hartogs  9563  card2on  9573  ackbij1  10256  cfub  10268  fin23lem27  10347  fin1a2lem11  10429  fin1a2lem13  10431  hsmexlem2  10446  zorn2lem4  10518  ondomon  10582  gchina  10718  intgru  10833  ingru  10834  addclprlem2  11036  psslinpr  11050  ltexprlem3  11057  ltexprlem4  11058  reclem2pr  11067  suplem1pr  11071  sup2  12203  nnind  12263  nnunb  12502  uzind  12690  xmullem2  13286  xrsupsslem  13328  xrinfmsslem  13329  seqof  14082  hashfacen  14477  sswrd  14545  wrdind  14745  wrd2ind  14746  pfxccatin12lem2  14754  cau3lem  15378  caubnd  15382  sumodd  16412  vdwnnlem2  17021  ramub2  17039  fthres2  17952  oduprs  18317  odupos  18343  cycsubm  19190  lsmdisj2  19668  gsumxp2  19966  pgpfac1lem3  20065  nrhmzr  20502  subrgdvds  20551  lspdisj  21091  lspprat  21119  lbsextlem2  21125  ocv2ss  21638  ocvin  21639  coe1fzgsumd  22247  evl1gsumd  22300  tgcl  22912  epttop  22952  cmpsub  23343  tgcmp  23344  hauscmplem  23349  dfconn2  23362  llyss  23422  nllyss  23423  locfincmp  23469  txcnpi  23551  txcnp  23563  snfil  23807  fgcl  23821  filconn  23826  filuni  23828  cfinfil  23836  csdfil  23837  supfil  23838  ufildom1  23869  fin1aufil  23875  fmfnfmlem3  23899  ptcmplem2  23996  cldsubg  24054  iscau3  25235  iscau4  25236  caussi  25254  volfiniun  25505  plycj  26240  plycjOLD  26242  abelth  26408  wilthlem2  27036  lgsdir2lem4  27296  gausslemma2dlem0i  27332  gausslemma2dlem1a  27333  pntleml  27579  sltres  27631  nosupno  27672  noinfno  27687  nocvxmin  27747  noseqinds  28244  uhgr0vsize0  29223  cusgrfilem2  29441  uhgrvd00  29519  clwwisshclwws  30001  frcond3  30255  frgrncvvdeqlem2  30286  lpni  30466  ubthlem1  30856  chintcli  31317  h1de2i  31539  spansnm0i  31636  strlem1  32236  mdslmd1i  32315  reuxfrdf  32477  n0nsnel  32501  disjss1f  32558  disjpreima  32570  ssrelf  32600  suppss3  32706  nnindf  32803  wrdt2ind  32934  crefss  33885  esumpcvgval  34114  cbvex1v  35110  subgrtrl  35160  subgrpth  35161  subgrcycl  35162  derangenlem  35198  connpconn  35262  cvmsss2  35301  pocnv  35785  wzel  35847  in-ax8  36247  naim1  36412  naim2  36413  waj-ax  36437  lukshef-ax2  36438  bj-eximALT  36664  bj-sbievw1  36868  poimirlem26  37675  poimirlem30  37679  poimirlem32  37681  itg2addnclem  37700  ismtybndlem  37835  ablo4pnp  37909  isdrngo3  37988  keridl  38061  ispridl2  38067  ispridlc  38099  trcoss  38505  funALTVss  38722  disjss  38754  eldisjss  38761  prter1  38902  lshpdisj  39010  snatpsubN  39774  pmapglb2N  39795  pmapglb2xN  39796  elpaddn0  39824  ss2ab1  42237  sn-sup2  42489  nna4b4nsq  42658  mzpindd  42744  pellexlem3  42829  pellexlem5  42831  pellex  42833  2nn0ind  42944  lnr2i  43115  ofoaid1  43357  ofoaid2  43358  intabssd  43518  iunrelexpuztr  43718  hess  43779  frege52aid  43857  frege52b  43888  neik0pk1imk0  44046  relpmin  44952  rankrelp  44960  n0nsn2el  47034  imasetpreimafvbijlemfv1  47397  isubgredg  47859  stgrusgra  47951  isubgr3stgrlem6  47963  iinfsubc  49005  elsetrecslem  49543