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  1446  3orim123d  1447  sbi1  2077  moim  2545  mo3  2565  2euswapv  2631  2euswap  2646  exists2  2663  nelcon3d  3041  ral2imi  3077  ralimdv2  3147  reximdv2  3148  reximd2a  3248  moeq3  3672  rmoim  3700  2reuswap  3706  2reuswap2  3707  2rmoswap  3721  ssel  3929  sstr2OLD  3943  ssrexf  4002  ssrmof  4003  ssralv  4004  ssrexv  4005  ss2abim  4014  ss2abdv  4019  rabss3d  4035  sscon  4097  ssdif  4098  unss1  4139  ssrin  4196  difin0ss  4327  r19.2z  4454  sspw  4567  uniss  4873  ssuni  4890  intssuni  4927  iinssiun  4962  iunss1  4963  iinss1  4964  ss2iun  4967  iunxdif3  5052  disjss2  5070  disjss1  5073  disjss3  5099  ssbrd  5143  poss  5544  pofun  5560  soss  5562  frss  5598  sess1  5599  sess2  5600  wess  5620  relss  5741  ssrel2  5744  ssrelrel  5755  relop  5809  dmss  5861  dmcosseq  5937  dmcosseqOLD  5938  dmcosseqOLDOLD  5939  funss  6521  f1imadifssran  6588  fss  6688  fun  6706  brprcneu  6834  brprcneuALT  6835  f1eqcocnv  7259  isores3  7293  isomin  7295  isopolem  7303  isosolem  7305  isowe2  7308  ovmpos  7518  dfwe2  7731  epweon  7732  onint  7747  orduniorsuc  7784  trom  7829  finds  7850  finds2  7852  f1oweALT  7928  tposfn2  8202  tposfo2  8203  tposf1o2  8206  fprlem2  8255  smores  8296  tz7.48lem  8384  tz7.48-3  8387  oaass  8500  brinxper  8677  iiner  8740  xpdom2  9014  ssenen  9093  pssnn  9107  hartogs  9463  card2on  9473  ackbij1  10161  cfub  10173  fin23lem27  10252  fin1a2lem11  10334  fin1a2lem13  10336  hsmexlem2  10351  zorn2lem4  10423  ondomon  10487  gchina  10624  intgru  10739  ingru  10740  addclprlem2  10942  psslinpr  10956  ltexprlem3  10963  ltexprlem4  10964  reclem2pr  10973  suplem1pr  10977  sup2  12112  nnind  12177  nnunb  12411  uzind  12598  xmullem2  13194  xrsupsslem  13236  xrinfmsslem  13237  seqof  13996  hashfacen  14391  sswrd  14459  wrdind  14659  wrd2ind  14660  pfxccatin12lem2  14668  cau3lem  15292  caubnd  15296  sumodd  16329  vdwnnlem2  16938  ramub2  16956  fthres2  17872  oduprs  18237  odupos  18263  chnrss  18552  chndss  18553  cycsubm  19148  lsmdisj2  19628  gsumxp2  19926  pgpfac1lem3  20025  nrhmzr  20487  subrgdvds  20536  lspdisj  21097  lspprat  21125  lbsextlem2  21131  ocv2ss  21645  ocvin  21646  coe1fzgsumd  22265  evl1gsumd  22318  tgcl  22930  epttop  22970  cmpsub  23361  tgcmp  23362  hauscmplem  23367  dfconn2  23380  llyss  23440  nllyss  23441  locfincmp  23487  txcnpi  23569  txcnp  23581  snfil  23825  fgcl  23839  filconn  23844  filuni  23846  cfinfil  23854  csdfil  23855  supfil  23856  ufildom1  23887  fin1aufil  23893  fmfnfmlem3  23917  ptcmplem2  24014  cldsubg  24072  iscau3  25251  iscau4  25252  caussi  25270  volfiniun  25521  plycj  26256  plycjOLD  26258  abelth  26424  wilthlem2  27052  lgsdir2lem4  27312  gausslemma2dlem0i  27348  gausslemma2dlem1a  27349  pntleml  27595  ltsres  27647  nosupno  27688  noinfno  27703  noseqinds  28306  uhgr0vsize0  29330  cusgrfilem2  29548  uhgrvd00  29626  clwwisshclwws  30108  frcond3  30362  frgrncvvdeqlem2  30393  lpni  30574  ubthlem1  30964  chintcli  31425  h1de2i  31647  spansnm0i  31744  strlem1  32344  mdslmd1i  32423  reuxfrdf  32583  n0nsnel  32608  disjss1f  32665  disjpreima  32677  ssrelf  32711  suppss3  32819  nnindf  32917  wrdt2ind  33052  crefss  34033  esumpcvgval  34262  cbvex1v  35256  r1filim  35287  onvf1odlem4  35328  subgrtrl  35355  subgrpth  35356  subgrcycl  35357  derangenlem  35393  connpconn  35457  cvmsss2  35496  pocnv  35985  wzel  36044  in-ax8  36446  naim1  36611  naim2  36612  waj-ax  36636  lukshef-ax2  36637  bj-exim  36872  bj-sbievw1  37120  poimirlem26  37926  poimirlem30  37930  poimirlem32  37932  itg2addnclem  37951  ismtybndlem  38086  ablo4pnp  38160  isdrngo3  38239  keridl  38312  ispridl2  38318  ispridlc  38350  trcoss  38852  funALTVss  39064  disjss  39111  eldisjss  39118  prter1  39284  lshpdisj  39392  snatpsubN  40155  pmapglb2N  40176  pmapglb2xN  40177  elpaddn0  40205  sn-sup2  42890  nna4b4nsq  43047  mzpindd  43132  pellexlem3  43217  pellexlem5  43219  pellex  43221  2nn0ind  43331  lnr2i  43502  ofoaid1  43744  ofoaid2  43745  intabssd  43904  iunrelexpuztr  44104  hess  44165  frege52aid  44243  frege52b  44274  neik0pk1imk0  44432  relpmin  45337  rankrelp  45345  n0nsn2el  47414  imasetpreimafvbijlemfv1  47792  isubgredg  48255  stgrusgra  48348  isubgr3stgrlem6  48360  iinfsubc  49446  elsetrecslem  50087