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  2072  moim  2537  mo3  2557  2euswapv  2623  2euswap  2638  exists2  2655  nelcon3d  3033  ral2imi  3068  ralimdv2  3138  reximdv2  3139  reximd2a  3239  moeq3  3672  rmoim  3700  2reuswap  3706  2reuswap2  3707  2rmoswap  3721  ssel  3929  sstr2OLD  3943  ssrexf  4002  ssrmof  4003  ssralv  4004  ssrexv  4005  ss2abdv  4018  rabss3d  4032  sscon  4094  ssdif  4095  unss1  4136  ssrin  4193  difin0ss  4324  r19.2z  4446  sspw  4562  uniss  4866  ssuni  4883  intssuni  4920  iinssiun  4955  iunss1  4956  iinss1  4957  ss2iun  4960  iunxdif3  5044  disjss2  5062  disjss1  5065  disjss3  5091  ssbrd  5135  poss  5529  pofun  5545  soss  5547  frss  5583  sess1  5584  sess2  5585  wess  5605  relss  5725  ssrel2  5728  ssrelrel  5739  relop  5793  dmss  5845  dmcosseq  5919  dmcosseqOLD  5920  dmcosseqOLDOLD  5921  funss  6501  f1imadifssran  6568  fss  6668  fun  6686  brprcneu  6812  brprcneuALT  6813  f1eqcocnv  7238  isores3  7272  isomin  7274  isopolem  7282  isosolem  7284  isowe2  7287  ovmpos  7497  dfwe2  7710  epweon  7711  onint  7726  orduniorsuc  7763  trom  7808  finds  7829  finds2  7831  f1oweALT  7907  tposfn2  8181  tposfo2  8182  tposf1o2  8185  fprlem2  8234  smores  8275  tz7.48lem  8363  tz7.48-3  8366  oaass  8479  brinxper  8654  iiner  8716  xpdom2  8989  ssenen  9068  pssnn  9082  hartogs  9436  card2on  9446  ackbij1  10131  cfub  10143  fin23lem27  10222  fin1a2lem11  10304  fin1a2lem13  10306  hsmexlem2  10321  zorn2lem4  10393  ondomon  10457  gchina  10593  intgru  10708  ingru  10709  addclprlem2  10911  psslinpr  10925  ltexprlem3  10932  ltexprlem4  10933  reclem2pr  10942  suplem1pr  10946  sup2  12081  nnind  12146  nnunb  12380  uzind  12568  xmullem2  13167  xrsupsslem  13209  xrinfmsslem  13210  seqof  13966  hashfacen  14361  sswrd  14429  wrdind  14628  wrd2ind  14629  pfxccatin12lem2  14637  cau3lem  15262  caubnd  15266  sumodd  16299  vdwnnlem2  16908  ramub2  16926  fthres2  17841  oduprs  18206  odupos  18232  cycsubm  19081  lsmdisj2  19561  gsumxp2  19859  pgpfac1lem3  19958  nrhmzr  20422  subrgdvds  20471  lspdisj  21032  lspprat  21060  lbsextlem2  21066  ocv2ss  21580  ocvin  21581  coe1fzgsumd  22189  evl1gsumd  22242  tgcl  22854  epttop  22894  cmpsub  23285  tgcmp  23286  hauscmplem  23291  dfconn2  23304  llyss  23364  nllyss  23365  locfincmp  23411  txcnpi  23493  txcnp  23505  snfil  23749  fgcl  23763  filconn  23768  filuni  23770  cfinfil  23778  csdfil  23779  supfil  23780  ufildom1  23811  fin1aufil  23817  fmfnfmlem3  23841  ptcmplem2  23938  cldsubg  23996  iscau3  25176  iscau4  25177  caussi  25195  volfiniun  25446  plycj  26181  plycjOLD  26183  abelth  26349  wilthlem2  26977  lgsdir2lem4  27237  gausslemma2dlem0i  27273  gausslemma2dlem1a  27274  pntleml  27520  sltres  27572  nosupno  27613  noinfno  27628  noseqinds  28192  uhgr0vsize0  29184  cusgrfilem2  29402  uhgrvd00  29480  clwwisshclwws  29959  frcond3  30213  frgrncvvdeqlem2  30244  lpni  30424  ubthlem1  30814  chintcli  31275  h1de2i  31497  spansnm0i  31594  strlem1  32194  mdslmd1i  32273  reuxfrdf  32435  n0nsnel  32459  disjss1f  32516  disjpreima  32528  ssrelf  32560  suppss3  32668  nnindf  32765  wrdt2ind  32896  crefss  33822  esumpcvgval  34051  cbvex1v  35047  onvf1odlem4  35089  subgrtrl  35116  subgrpth  35117  subgrcycl  35118  derangenlem  35154  connpconn  35218  cvmsss2  35257  pocnv  35746  wzel  35808  in-ax8  36208  naim1  36373  naim2  36374  waj-ax  36398  lukshef-ax2  36399  bj-eximALT  36625  bj-sbievw1  36829  poimirlem26  37636  poimirlem30  37640  poimirlem32  37642  itg2addnclem  37661  ismtybndlem  37796  ablo4pnp  37870  isdrngo3  37949  keridl  38022  ispridl2  38028  ispridlc  38060  trcoss  38469  funALTVss  38687  disjss  38719  eldisjss  38726  prter1  38868  lshpdisj  38976  snatpsubN  39739  pmapglb2N  39760  pmapglb2xN  39761  elpaddn0  39789  ss2ab1  42202  sn-sup2  42474  nna4b4nsq  42643  mzpindd  42729  pellexlem3  42814  pellexlem5  42816  pellex  42818  2nn0ind  42928  lnr2i  43099  ofoaid1  43341  ofoaid2  43342  intabssd  43502  iunrelexpuztr  43702  hess  43763  frege52aid  43841  frege52b  43872  neik0pk1imk0  44030  relpmin  44936  rankrelp  44944  n0nsn2el  47019  imasetpreimafvbijlemfv1  47397  isubgredg  47860  stgrusgra  47953  isubgr3stgrlem6  47965  iinfsubc  49053  elsetrecslem  49694