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  1442  3orim123d  1443  sbi1  2073  moim  2537  mo3  2557  2euswapv  2625  2euswap  2640  exists2  2656  nelcon3d  3049  ral2imi  3084  ralimdv2  3162  reximdv2  3163  reximd2a  3265  moeq3  3708  rmoim  3736  2reuswap  3742  2reuswap2  3743  2rmoswap  3757  ssel  3975  sselOLD  3976  sstr2  3989  ssrexf  4048  ssrmof  4049  ss2abdvALT  4061  rabss3d  4079  sscon  4138  ssdif  4139  unss1  4179  ssrin  4233  difin0ss  4368  r19.2z  4494  sspw  4613  uniss  4916  ssuni  4936  intssuni  4974  iinssiun  5010  iunss1  5011  iinss1  5012  ss2iun  5015  iunxdif3  5098  disjss2  5116  disjss1  5119  disjss3  5147  ssbrd  5191  poss  5590  pofun  5606  soss  5608  frss  5643  sess1  5644  sess2  5645  wess  5663  relss  5781  ssrel2  5785  ssrelrel  5796  relop  5850  dmss  5902  dmcosseq  5972  funss  6567  fss  6734  fun  6753  brprcneu  6881  brprcneuALT  6882  f1eqcocnv  7302  f1eqcocnvOLD  7303  isores3  7335  isomin  7337  isopolem  7345  isosolem  7347  isowe2  7350  ovmpos  7559  dfwe2  7765  epweon  7766  onint  7782  orduniorsuc  7822  trom  7868  finds  7893  finds2  7895  f1oweALT  7963  tposfn2  8239  tposfo2  8240  tposf1o2  8243  fprlem2  8292  smores  8358  tz7.48lem  8447  tz7.48-3  8450  oaass  8567  iiner  8789  xpdom2  9073  ssenen  9157  pssnn  9174  pssnnOLD  9271  hartogs  9545  card2on  9555  ackbij1  10239  cfub  10250  fin23lem27  10329  fin1a2lem11  10411  fin1a2lem13  10413  hsmexlem2  10428  zorn2lem4  10500  ondomon  10564  gchina  10700  intgru  10815  ingru  10816  addclprlem2  11018  psslinpr  11032  ltexprlem3  11039  ltexprlem4  11040  reclem2pr  11049  suplem1pr  11053  sup2  12177  nnind  12237  nnunb  12475  uzind  12661  xmullem2  13251  xrsupsslem  13293  xrinfmsslem  13294  seqof  14032  hashfacen  14420  hashfacenOLD  14421  sswrd  14479  wrdind  14679  wrd2ind  14680  pfxccatin12lem2  14688  cau3lem  15308  caubnd  15312  sumodd  16338  vdwnnlem2  16936  ramub2  16954  fthres2  17890  odupos  18288  cycsubm  19121  lsmdisj2  19595  gsumxp2  19893  pgpfac1lem3  19992  subrgdvds  20480  lspdisj  20887  lspprat  20915  lbsextlem2  20921  ocv2ss  21449  ocvin  21450  coe1fzgsumd  22059  evl1gsumd  22109  tgcl  22705  epttop  22745  cmpsub  23137  tgcmp  23138  hauscmplem  23143  dfconn2  23156  llyss  23216  nllyss  23217  locfincmp  23263  txcnpi  23345  txcnp  23357  snfil  23601  fgcl  23615  filconn  23620  filuni  23622  cfinfil  23630  csdfil  23631  supfil  23632  ufildom1  23663  fin1aufil  23669  fmfnfmlem3  23693  ptcmplem2  23790  cldsubg  23848  iscau3  25039  iscau4  25040  caussi  25058  volfiniun  25309  plycj  26041  abelth  26204  wilthlem2  26824  lgsdir2lem4  27082  gausslemma2dlem0i  27118  gausslemma2dlem1a  27119  pntleml  27365  sltres  27416  nosupno  27457  noinfno  27472  nocvxmin  27531  uhgr0vsize0  28778  cusgrfilem2  28995  uhgrvd00  29073  clwwisshclwws  29550  frcond3  29804  frgrncvvdeqlem2  29835  lpni  30015  ubthlem1  30405  chintcli  30866  h1de2i  31088  spansnm0i  31185  strlem1  31785  mdslmd1i  31864  reuxfrdf  32013  disjss1f  32085  disjpreima  32097  ssrelf  32126  suppss3  32231  nnindf  32307  wrdt2ind  32399  oduprs  32416  crefss  33142  esumpcvgval  33389  subgrtrl  34437  subgrpth  34438  subgrcycl  34439  derangenlem  34475  connpconn  34539  cvmsss2  34578  pocnv  35052  wzel  35115  naim1  35590  naim2  35591  waj-ax  35615  lukshef-ax2  35616  bj-eximALT  35834  bj-sbievw1  36040  poimirlem26  36830  poimirlem30  36834  poimirlem32  36836  itg2addnclem  36855  ismtybndlem  36990  ablo4pnp  37064  isdrngo3  37143  keridl  37216  ispridl2  37222  ispridlc  37254  trcoss  37668  funALTVss  37885  disjss  37917  eldisjss  37924  prter1  38065  lshpdisj  38173  snatpsubN  38937  pmapglb2N  38958  pmapglb2xN  38959  elpaddn0  38987  ss2ab1  41355  sn-sup2  41657  nna4b4nsq  41717  mzpindd  41799  pellexlem3  41884  pellexlem5  41886  pellex  41888  2nn0ind  41999  lnr2i  42173  ofoaid1  42423  ofoaid2  42424  intabssd  42585  iunrelexpuztr  42785  hess  42846  frege52aid  42924  frege52b  42955  neik0pk1imk0  43113  n0nsn2el  46046  imasetpreimafvbijlemfv1  46382  nrhmzr  46923  elsetrecslem  47844