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 241	. 2 ⊢ (𝜑 → (𝜃 → 𝜒))
4		3imtr4g.3	. 2 ⊢ (𝜏 ↔ 𝜒)
5	3, 4	imbitrrdi 251	1 ⊢ (𝜑 → (𝜃 → 𝜏))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  3anim123d  1444  3orim123d  1445  sbi1  2075  moim  2539  mo3  2559  2euswapv  2627  2euswap  2642  exists2  2658  nelcon3d  3051  ral2imi  3086  ralimdv2  3164  reximdv2  3165  reximd2a  3267  moeq3  3709  rmoim  3737  2reuswap  3743  2reuswap2  3744  2rmoswap  3758  ssel  3976  sselOLD  3977  sstr2  3990  ssrexf  4049  ssrmof  4050  ss2abdvALT  4062  rabss3d  4080  sscon  4139  ssdif  4140  unss1  4180  ssrin  4234  difin0ss  4369  r19.2z  4495  sspw  4614  uniss  4917  ssuni  4937  intssuni  4975  iinssiun  5011  iunss1  5012  iinss1  5013  ss2iun  5016  iunxdif3  5099  disjss2  5117  disjss1  5120  disjss3  5148  ssbrd  5192  poss  5591  pofun  5607  soss  5609  frss  5644  sess1  5645  sess2  5646  wess  5664  relss  5782  ssrel2  5786  ssrelrel  5797  relop  5851  dmss  5903  dmcosseq  5973  funss  6568  fss  6735  fun  6754  brprcneu  6882  brprcneuALT  6883  f1eqcocnv  7299  f1eqcocnvOLD  7300  isores3  7332  isomin  7334  isopolem  7342  isosolem  7344  isowe2  7347  ovmpos  7556  dfwe2  7761  epweon  7762  onint  7778  orduniorsuc  7818  trom  7864  finds  7889  finds2  7891  f1oweALT  7959  tposfn2  8233  tposfo2  8234  tposf1o2  8237  fprlem2  8286  smores  8352  tz7.48lem  8441  tz7.48-3  8444  oaass  8561  iiner  8783  xpdom2  9067  ssenen  9151  pssnn  9168  pssnnOLD  9265  hartogs  9539  card2on  9549  ackbij1  10233  cfub  10244  fin23lem27  10323  fin1a2lem11  10405  fin1a2lem13  10407  hsmexlem2  10422  zorn2lem4  10494  ondomon  10558  gchina  10694  intgru  10809  ingru  10810  addclprlem2  11012  psslinpr  11026  ltexprlem3  11033  ltexprlem4  11034  reclem2pr  11043  suplem1pr  11047  sup2  12170  nnind  12230  nnunb  12468  uzind  12654  xmullem2  13244  xrsupsslem  13286  xrinfmsslem  13287  seqof  14025  hashfacen  14413  hashfacenOLD  14414  sswrd  14472  wrdind  14672  wrd2ind  14673  pfxccatin12lem2  14681  cau3lem  15301  caubnd  15305  sumodd  16331  vdwnnlem2  16929  ramub2  16947  fthres2  17883  odupos  18281  cycsubm  19079  lsmdisj2  19550  gsumxp2  19848  pgpfac1lem3  19947  subrgdvds  20333  lspdisj  20738  lspprat  20766  lbsextlem2  20772  ocv2ss  21226  ocvin  21227  coe1fzgsumd  21826  evl1gsumd  21876  tgcl  22472  epttop  22512  cmpsub  22904  tgcmp  22905  hauscmplem  22910  dfconn2  22923  llyss  22983  nllyss  22984  locfincmp  23030  txcnpi  23112  txcnp  23124  snfil  23368  fgcl  23382  filconn  23387  filuni  23389  cfinfil  23397  csdfil  23398  supfil  23399  ufildom1  23430  fin1aufil  23436  fmfnfmlem3  23460  ptcmplem2  23557  cldsubg  23615  iscau3  24795  iscau4  24796  caussi  24814  volfiniun  25064  plycj  25791  abelth  25953  wilthlem2  26573  lgsdir2lem4  26831  gausslemma2dlem0i  26867  gausslemma2dlem1a  26868  pntleml  27114  sltres  27165  nosupno  27206  noinfno  27221  nocvxmin  27280  uhgr0vsize0  28496  cusgrfilem2  28713  uhgrvd00  28791  clwwisshclwws  29268  frcond3  29522  frgrncvvdeqlem2  29553  lpni  29733  ubthlem1  30123  chintcli  30584  h1de2i  30806  spansnm0i  30903  strlem1  31503  mdslmd1i  31582  reuxfrdf  31731  disjss1f  31803  disjpreima  31815  ssrelf  31844  suppss3  31949  nnindf  32025  wrdt2ind  32117  oduprs  32134  crefss  32829  esumpcvgval  33076  subgrtrl  34124  subgrpth  34125  subgrcycl  34126  derangenlem  34162  connpconn  34226  cvmsss2  34265  pocnv  34733  wzel  34796  naim1  35274  naim2  35275  waj-ax  35299  lukshef-ax2  35300  bj-eximALT  35518  bj-sbievw1  35724  poimirlem26  36514  poimirlem30  36518  poimirlem32  36520  itg2addnclem  36539  ismtybndlem  36674  ablo4pnp  36748  isdrngo3  36827  keridl  36900  ispridl2  36906  ispridlc  36938  trcoss  37352  funALTVss  37569  disjss  37601  eldisjss  37608  prter1  37749  lshpdisj  37857  snatpsubN  38621  pmapglb2N  38642  pmapglb2xN  38643  elpaddn0  38671  ss2ab1  41036  sn-sup2  41342  nna4b4nsq  41402  mzpindd  41484  pellexlem3  41569  pellexlem5  41571  pellex  41573  2nn0ind  41684  lnr2i  41858  ofoaid1  42108  ofoaid2  42109  intabssd  42270  iunrelexpuztr  42470  hess  42531  frege52aid  42609  frege52b  42640  neik0pk1imk0  42798  n0nsn2el  45735  imasetpreimafvbijlemfv1  46071  nrhmzr  46647  elsetrecslem  47744