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  1466  3orim123d  1467  sbi1ALT  2106  moim  2573  mo3  2593  2euswapv  2659  2euswap  2674  exists2  2690  nelcon3d  3067  ral2imi  3103  ralimdv2  3173  reximdv2  3174  reximd2a  3274  moeq3  3677  rmoim  3705  2reuswap  3711  2reuswap2  3712  2rmoswap  3726  ssel  3932  ssrexf  4005  ssrmof  4006  ssralv  4007  ssrexv  4008  ss2abim  4015  ss2abdv  4020  rabss3d  4036  sscon  4098  ssdif  4099  unss1  4139  ssrin  4195  difin0ss  4328  r19.2z  4455  sspw  4568  uniss  4875  ssuni  4893  intssuni  4930  iinssiun  4965  iunss1  4966  iinss1  4967  ss2iun  4970  iunxdif3  5054  disjss2  5072  disjss1  5075  disjss3  5101  ssbrd  5145  poss  5559  pofun  5575  soss  5577  frss  5613  sess1  5614  sess2  5615  wess  5635  relss  5756  ssrel2  5759  ssrelrel  5770  relop  5824  dmss  5880  dmcosseq  5956  dmcosseqOLD  5957  dmcosseqOLDOLD  5958  funss  6542  f1imadifssran  6609  fss  6710  fun  6728  brprcneu  6859  brprcneuALT  6860  f1eqcocnv  7287  isores3  7321  isomin  7323  isopolem  7331  isosolem  7333  isowe2  7336  ovmpos  7546  dfwe2  7759  epweon  7760  onint  7775  orduniorsuc  7812  trom  7857  finds  7879  finds2  7881  f1oweALT  7955  tposfn2  8230  tposfo2  8231  tposf1o2  8234  fprlem2  8284  smores  8325  tz7.48lem  8414  tz7.48-3  8417  oaass  8532  brinxper  8710  iiner  8773  xpdom2  9046  ssenen  9125  pssnn  9139  hartogs  9494  card2on  9504  ackbij1  10195  cfub  10207  fin23lem27  10287  fin1a2lem11  10369  fin1a2lem13  10371  hsmexlem2  10386  zorn2lem4  10458  ondomon  10522  gchina  10659  intgru  10774  ingru  10775  addclprlem2  10977  psslinpr  10991  ltexprlem3  10998  ltexprlem4  10999  reclem2pr  11008  suplem1pr  11012  sup2  12150  nnind  12230  nnunb  12479  uzind  12667  xmullem2  13270  xrsupsslem  13312  xrinfmsslem  13313  seqof  14074  hashfacen  14469  sswrd  14537  wrdind  14737  wrd2ind  14738  pfxccatin12lem2  14746  cau3lem  15384  caubnd  15388  sumodd  16424  vdwnnlem2  17034  ramub2  17052  fthres2  17969  oduprs  18334  odupos  18360  chnrss  18649  chndss  18650  cycsubm  19245  lsmdisj2  19724  gsumxp2  20022  pgpfac1lem3  20121  nrhmzr  20589  subrgdvds  20638  lspdisj  21197  lspprat  21225  lbsextlem2  21231  ocv2ss  21727  ocvin  21728  coe1fzgsumd  22369  evl1gsumd  22422  tgcl  23031  epttop  23071  cmpsub  23462  tgcmp  23463  hauscmplem  23468  dfconn2  23481  llyss  23541  nllyss  23542  locfincmp  23588  txcnpi  23670  txcnp  23682  snfil  23926  fgcl  23940  filconn  23945  filuni  23947  cfinfil  23955  csdfil  23956  supfil  23957  ufildom1  23988  fin1aufil  23994  fmfnfmlem3  24018  ptcmplem2  24115  cldsubg  24173  iscau3  25342  iscau4  25343  caussi  25361  volfiniun  25611  plycj  26339  plycjOLD  26341  abelth  26506  wilthlem2  27135  lgsdir2lem4  27394  gausslemma2dlem0i  27430  gausslemma2dlem1a  27431  pntleml  27677  ltsres  27728  nosupno  27769  noinfno  27784  noseqinds  28388  plngrotlem2  28997  uhgr0vsize0  29442  cusgrfilem2  29659  uhgrvd00  29737  clwwisshclwws  30219  frcond3  30473  frgrncvvdeqlem2  30504  lpni  30685  ubthlem1  31075  chintcli  31536  h1de2i  31758  spansnm0i  31855  strlem1  32455  mdslmd1i  32534  reuxfrdf  32692  n0nsnel  32716  disjss1f  32774  disjpreima  32786  ssrelf  32819  suppss3  32927  nnindf  33024  wrdt2ind  33133  crefss  34148  esumpcvgval  34377  cbvex1v  35371  r1filim  35404  onvf1odlem4  35453  subgrtrl  35488  subgrpth  35489  subgrcycl  35490  derangenlem  35526  connpconn  35590  cvmsss2  35629  pocnv  36118  wzel  36177  in-ax8  36589  naim1  36754  naim2  36755  waj-ax  36779  lukshef-ax2  36780  ttctr  36858  dfttc2g  36871  bj-exim  37087  bj-sbievw1  37335  wl-dfcleq  38013  poimirlem26  38150  poimirlem30  38154  poimirlem32  38156  itg2addnclem  38175  ismtybndlem  38310  ablo4pnp  38384  isdrngo3  38463  keridl  38536  ispridl2  38542  ispridlc  38574  trcoss  39076  funALTVss  39288  disjss  39335  eldisjss  39342  prter1  39508  lshpdisj  39616  snatpsubN  40379  pmapglb2N  40400  pmapglb2xN  40401  elpaddn0  40429  sn-sup2  43118  nna4b4nsq  43247  mzpindd  43332  pellexlem3  43413  pellexlem5  43415  pellex  43417  2nn0ind  43527  lnr2i  43698  ofoaid1  43940  ofoaid2  43941  intabssd  44100  iunrelexpuztr  44300  hess  44361  frege52aid  44439  frege52b  44470  neik0pk1imk0  44628  relpmin  45533  rankrelp  45541  n0nsn2el  47624  imasetpreimafvbijlemfv1  48014  isubgredg  48493  stgrusgra  48586  isubgr3stgrlem6  48598  iinfsubc  49684  elsetrecslem  50325