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  2076  moim  2542  mo3  2562  2euswapv  2628  2euswap  2643  exists2  2660  nelcon3d  3038  ral2imi  3073  ralimdv2  3143  reximdv2  3144  reximd2a  3244  moeq3  3668  rmoim  3696  2reuswap  3702  2reuswap2  3703  2rmoswap  3717  ssel  3925  sstr2OLD  3939  ssrexf  3998  ssrmof  3999  ssralv  4000  ssrexv  4001  ss2abdv  4015  rabss3d  4031  sscon  4093  ssdif  4094  unss1  4135  ssrin  4192  difin0ss  4323  r19.2z  4450  sspw  4563  uniss  4869  ssuni  4886  intssuni  4923  iinssiun  4958  iunss1  4959  iinss1  4960  ss2iun  4963  iunxdif3  5048  disjss2  5066  disjss1  5069  disjss3  5095  ssbrd  5139  poss  5532  pofun  5548  soss  5550  frss  5586  sess1  5587  sess2  5588  wess  5608  relss  5729  ssrel2  5732  ssrelrel  5743  relop  5797  dmss  5849  dmcosseq  5925  dmcosseqOLD  5926  dmcosseqOLDOLD  5927  funss  6509  f1imadifssran  6576  fss  6676  fun  6694  brprcneu  6822  brprcneuALT  6823  f1eqcocnv  7245  isores3  7279  isomin  7281  isopolem  7289  isosolem  7291  isowe2  7294  ovmpos  7504  dfwe2  7717  epweon  7718  onint  7733  orduniorsuc  7770  trom  7815  finds  7836  finds2  7838  f1oweALT  7914  tposfn2  8188  tposfo2  8189  tposf1o2  8192  fprlem2  8241  smores  8282  tz7.48lem  8370  tz7.48-3  8373  oaass  8486  brinxper  8662  iiner  8724  xpdom2  8998  ssenen  9077  pssnn  9091  hartogs  9447  card2on  9457  ackbij1  10145  cfub  10157  fin23lem27  10236  fin1a2lem11  10318  fin1a2lem13  10320  hsmexlem2  10335  zorn2lem4  10407  ondomon  10471  gchina  10608  intgru  10723  ingru  10724  addclprlem2  10926  psslinpr  10940  ltexprlem3  10947  ltexprlem4  10948  reclem2pr  10957  suplem1pr  10961  sup2  12096  nnind  12161  nnunb  12395  uzind  12582  xmullem2  13178  xrsupsslem  13220  xrinfmsslem  13221  seqof  13980  hashfacen  14375  sswrd  14443  wrdind  14643  wrd2ind  14644  pfxccatin12lem2  14652  cau3lem  15276  caubnd  15280  sumodd  16313  vdwnnlem2  16922  ramub2  16940  fthres2  17856  oduprs  18221  odupos  18247  chnrss  18536  chndss  18537  cycsubm  19129  lsmdisj2  19609  gsumxp2  19907  pgpfac1lem3  20006  nrhmzr  20468  subrgdvds  20517  lspdisj  21078  lspprat  21106  lbsextlem2  21112  ocv2ss  21626  ocvin  21627  coe1fzgsumd  22246  evl1gsumd  22299  tgcl  22911  epttop  22951  cmpsub  23342  tgcmp  23343  hauscmplem  23348  dfconn2  23361  llyss  23421  nllyss  23422  locfincmp  23468  txcnpi  23550  txcnp  23562  snfil  23806  fgcl  23820  filconn  23825  filuni  23827  cfinfil  23835  csdfil  23836  supfil  23837  ufildom1  23868  fin1aufil  23874  fmfnfmlem3  23898  ptcmplem2  23995  cldsubg  24053  iscau3  25232  iscau4  25233  caussi  25251  volfiniun  25502  plycj  26237  plycjOLD  26239  abelth  26405  wilthlem2  27033  lgsdir2lem4  27293  gausslemma2dlem0i  27329  gausslemma2dlem1a  27330  pntleml  27576  sltres  27628  nosupno  27669  noinfno  27684  noseqinds  28254  uhgr0vsize0  29261  cusgrfilem2  29479  uhgrvd00  29557  clwwisshclwws  30039  frcond3  30293  frgrncvvdeqlem2  30324  lpni  30504  ubthlem1  30894  chintcli  31355  h1de2i  31577  spansnm0i  31674  strlem1  32274  mdslmd1i  32353  reuxfrdf  32514  n0nsnel  32539  disjss1f  32596  disjpreima  32608  ssrelf  32642  suppss3  32751  nnindf  32849  wrdt2ind  32984  crefss  33955  esumpcvgval  34184  cbvex1v  35179  r1filim  35209  onvf1odlem4  35249  subgrtrl  35276  subgrpth  35277  subgrcycl  35278  derangenlem  35314  connpconn  35378  cvmsss2  35417  pocnv  35906  wzel  35965  in-ax8  36367  naim1  36532  naim2  36533  waj-ax  36557  lukshef-ax2  36558  bj-eximALT  36784  bj-sbievw1  36989  poimirlem26  37786  poimirlem30  37790  poimirlem32  37792  itg2addnclem  37811  ismtybndlem  37946  ablo4pnp  38020  isdrngo3  38099  keridl  38172  ispridl2  38178  ispridlc  38210  trcoss  38684  funALTVss  38897  disjss  38929  eldisjss  38936  prter1  39078  lshpdisj  39186  snatpsubN  39949  pmapglb2N  39970  pmapglb2xN  39971  elpaddn0  39999  ss2ab1  42417  sn-sup2  42688  nna4b4nsq  42845  mzpindd  42930  pellexlem3  43015  pellexlem5  43017  pellex  43019  2nn0ind  43129  lnr2i  43300  ofoaid1  43542  ofoaid2  43543  intabssd  43702  iunrelexpuztr  43902  hess  43963  frege52aid  44041  frege52b  44072  neik0pk1imk0  44230  relpmin  45135  rankrelp  45143  n0nsn2el  47213  imasetpreimafvbijlemfv1  47591  isubgredg  48054  stgrusgra  48147  isubgr3stgrlem6  48159  iinfsubc  49245  elsetrecslem  49886