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  3142  reximdv2  3143  reximd2a  3245  moeq3  3680  rmoim  3708  2reuswap  3714  2reuswap2  3715  2rmoswap  3729  ssel  3937  sstr2OLD  3951  ssrexf  4010  ssrmof  4011  ssralv  4012  ssrexv  4013  ss2abdv  4026  rabss3d  4040  sscon  4102  ssdif  4103  unss1  4144  ssrin  4201  difin0ss  4332  r19.2z  4454  sspw  4570  uniss  4875  ssuni  4892  intssuni  4930  iinssiun  4965  iunss1  4966  iinss1  4967  ss2iun  4970  iunxdif3  5054  disjss2  5072  disjss1  5075  disjss3  5101  ssbrd  5145  poss  5541  pofun  5557  soss  5559  frss  5595  sess1  5596  sess2  5597  wess  5617  relss  5736  ssrel2  5739  ssrelrel  5750  relop  5804  dmss  5856  dmcosseq  5929  dmcosseqOLD  5930  funss  6519  f1imadifssran  6586  fss  6686  fun  6704  brprcneu  6830  brprcneuALT  6831  f1eqcocnv  7258  isores3  7292  isomin  7294  isopolem  7302  isosolem  7304  isowe2  7307  ovmpos  7517  dfwe2  7730  epweon  7731  onint  7746  orduniorsuc  7785  trom  7831  finds  7852  finds2  7854  f1oweALT  7930  tposfn2  8204  tposfo2  8205  tposf1o2  8208  fprlem2  8257  smores  8298  tz7.48lem  8386  tz7.48-3  8389  oaass  8502  brinxper  8677  iiner  8739  xpdom2  9013  ssenen  9092  pssnn  9109  hartogs  9473  card2on  9483  ackbij1  10166  cfub  10178  fin23lem27  10257  fin1a2lem11  10339  fin1a2lem13  10341  hsmexlem2  10356  zorn2lem4  10428  ondomon  10492  gchina  10628  intgru  10743  ingru  10744  addclprlem2  10946  psslinpr  10960  ltexprlem3  10967  ltexprlem4  10968  reclem2pr  10977  suplem1pr  10981  sup2  12115  nnind  12180  nnunb  12414  uzind  12602  xmullem2  13201  xrsupsslem  13243  xrinfmsslem  13244  seqof  14000  hashfacen  14395  sswrd  14463  wrdind  14663  wrd2ind  14664  pfxccatin12lem2  14672  cau3lem  15297  caubnd  15301  sumodd  16334  vdwnnlem2  16943  ramub2  16961  fthres2  17876  oduprs  18241  odupos  18267  cycsubm  19116  lsmdisj2  19596  gsumxp2  19894  pgpfac1lem3  19993  nrhmzr  20457  subrgdvds  20506  lspdisj  21067  lspprat  21095  lbsextlem2  21101  ocv2ss  21615  ocvin  21616  coe1fzgsumd  22224  evl1gsumd  22277  tgcl  22889  epttop  22929  cmpsub  23320  tgcmp  23321  hauscmplem  23326  dfconn2  23339  llyss  23399  nllyss  23400  locfincmp  23446  txcnpi  23528  txcnp  23540  snfil  23784  fgcl  23798  filconn  23803  filuni  23805  cfinfil  23813  csdfil  23814  supfil  23815  ufildom1  23846  fin1aufil  23852  fmfnfmlem3  23876  ptcmplem2  23973  cldsubg  24031  iscau3  25211  iscau4  25212  caussi  25230  volfiniun  25481  plycj  26216  plycjOLD  26218  abelth  26384  wilthlem2  27012  lgsdir2lem4  27272  gausslemma2dlem0i  27308  gausslemma2dlem1a  27309  pntleml  27555  sltres  27607  nosupno  27648  noinfno  27663  noseqinds  28227  uhgr0vsize0  29219  cusgrfilem2  29437  uhgrvd00  29515  clwwisshclwws  29994  frcond3  30248  frgrncvvdeqlem2  30279  lpni  30459  ubthlem1  30849  chintcli  31310  h1de2i  31532  spansnm0i  31629  strlem1  32229  mdslmd1i  32308  reuxfrdf  32470  n0nsnel  32494  disjss1f  32551  disjpreima  32563  ssrelf  32593  suppss3  32697  nnindf  32794  wrdt2ind  32925  crefss  33832  esumpcvgval  34061  cbvex1v  35057  onvf1odlem4  35086  subgrtrl  35113  subgrpth  35114  subgrcycl  35115  derangenlem  35151  connpconn  35215  cvmsss2  35254  pocnv  35743  wzel  35805  in-ax8  36205  naim1  36370  naim2  36371  waj-ax  36395  lukshef-ax2  36396  bj-eximALT  36622  bj-sbievw1  36826  poimirlem26  37633  poimirlem30  37637  poimirlem32  37639  itg2addnclem  37658  ismtybndlem  37793  ablo4pnp  37867  isdrngo3  37946  keridl  38019  ispridl2  38025  ispridlc  38057  trcoss  38466  funALTVss  38684  disjss  38716  eldisjss  38723  prter1  38865  lshpdisj  38973  snatpsubN  39737  pmapglb2N  39758  pmapglb2xN  39759  elpaddn0  39787  ss2ab1  42200  sn-sup2  42472  nna4b4nsq  42641  mzpindd  42727  pellexlem3  42812  pellexlem5  42814  pellex  42816  2nn0ind  42927  lnr2i  43098  ofoaid1  43340  ofoaid2  43341  intabssd  43501  iunrelexpuztr  43701  hess  43762  frege52aid  43840  frege52b  43871  neik0pk1imk0  44029  relpmin  44935  rankrelp  44943  n0nsn2el  47019  imasetpreimafvbijlemfv1  47397  isubgredg  47859  stgrusgra  47951  isubgr3stgrlem6  47963  iinfsubc  49040  elsetrecslem  49681