Theorem 3imtr4g 299

Description: More general version of 3imtr4i 295. 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 245	. 2 ⊢ (𝜑 → (𝜃 → 𝜒))
4		3imtr4g.3	. 2 ⊢ (𝜏 ↔ 𝜒)
5	3, 4	imbitrrdi 255	1 ⊢ (𝜑 → (𝜃 → 𝜏))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  3anim123d  1472  3orim123d  1473  sbi1  2110  moim  2572  mo3  2592  2euswapv  2658  2euswap  2673  exists2  2689  nelcon3d  3069  ral2imi  3105  ralimdv2  3175  reximdv2  3176  reximd2a  3276  moeq3  3673  rmoim  3701  2reuswap  3707  2reuswap2  3708  2rmoswap  3722  ssel  3907  ssrexf  3980  ssrmof  3981  ssralv  3982  ssrexv  3983  ss2abim  3988  ss2abdv  3993  rabss3d  4009  sscon  4082  ssdif  4083  ssrin  4141  unss1  4186  difin0ss  4324  r19.2z  4458  sspw  4571  uniss  4878  ssuni  4896  intssuni  4933  iinssiun  4968  iunss1  4969  iinss1  4970  ss2iun  4973  iunxdif3  5058  disjss2  5076  disjss1  5079  disjss3  5105  ssbrd  5151  poss  5565  pofun  5581  soss  5583  frss  5619  sess1  5620  sess2  5621  wess  5641  relss  5763  ssrel2  5766  ssrelrel  5777  relop  5833  dmss  5890  dmcosseq  5966  dmcosseqOLD  5967  funss  6575  fss  6745  fun  6763  brprcneu  6895  brprcneuALT  6896  f1eqcocnv  7329  isores3  7363  isomin  7365  isopolem  7373  isosolem  7375  isowe2  7378  ovmpos  7589  dfwe2  7809  epweon  7810  onint  7825  orduniorsuc  7862  trom  7907  finds  7929  finds2  7931  f1oweALT  8005  tposfn2  8290  tposfo2  8291  tposf1o2  8294  fprlem2  8344  smores  8385  tz7.48lemOLD  8476  tz7.48-3  8479  oaass  8594  brinxper  8772  iiner  8835  xpdom2  9116  ssenen  9195  pssnn  9209  hartogs  9562  card2on  9572  elhf4  9936  ackbij1  10339  cfub  10350  fin23lem27  10430  fin1a2lem11  10512  fin1a2lem13  10514  hsmexlem2  10529  zorn2lem4  10601  ondomon  10671  gchina  10808  intgru  10923  ingru  10924  addclprlem2  11126  psslinpr  11140  ltexprlem3  11147  ltexprlem4  11148  reclem2pr  11157  suplem1pr  11161  sup2  12297  nnind  12377  nnunb  12626  uzind  12815  xmullem2  13419  xrsupsslem  13461  xrinfmsslem  13462  seqof  14226  hashfacen  14623  sswrd  14691  wrdind  14896  wrd2ind  14897  pfxccatin12lem2  14905  cau3lem  15548  caubnd  15552  sumodd  16584  vdwnnlem2  17200  ramub2  17218  fthres2  18135  oduprs  18500  odupos  18526  chnrss  18815  chndss  18816  cycsubm  19443  lsmdisj2  19923  gsumxp2  20221  pgpfac1lem3  20320  nrhmzr  20816  subrgdvds  20865  isdrng5  21035  lspdisj  21430  lspprat  21458  lbsextlem2  21464  ocv2ss  22006  ocvin  22007  coe1fzgsumd  22649  evl1gsumd  22702  tgcl  23314  epttop  23354  cmpsub  23745  tgcmp  23746  hauscmplem  23751  dfconn2  23764  llyss  23825  nllyss  23826  locfincmp  23872  txcnpi  23954  txcnp  23966  snfil  24210  fgcl  24224  filconn  24229  filuni  24231  cfinfil  24239  csdfil  24240  supfil  24241  ufildom1  24272  fin1aufil  24278  fmfnfmlem3  24302  ptcmplem2  24399  cldsubg  24457  iscau3  25626  iscau4  25627  caussi  25645  volfiniun  25895  plycj  26623  abelth  26795  wilthlem2  27423  lgsdir2lem4  27682  gausslemma2dlem0i  27718  gausslemma2dlem1a  27719  pntleml  27965  ltsres  28046  nosupno  28087  noinfno  28102  noseqinds  28706  plngrotlem2  29293  uhgr0vsize0  29847  cusgrfilem2  30064  uhgrvd00  30142  subgrtrl  30321  subgrpth  30383  subgrcycl  30412  clwwisshclwws  30633  frcond3  30897  frgrncvvdeqlem2  30928  lpni  31109  ubthlem1  31499  chintcli  31960  h1de2i  32182  spansnm0i  32279  strlem1  32879  mdslmd1i  32958  reuxfrdf  33156  n0nsnel  33180  disjss1f  33235  disjpreima  33247  ssrelf  33278  suppss3  33382  nnindf  33478  wrdt2ind  33583  crefss  34548  esumpcvgval  34777  cbvex1v  35771  r1filim  35810  onvf1odlem4  36033  derangenlem  36102  connpconn  36166  cvmsss2  36205  pocnv  36705  wzel  36763  in-ax8  37190  naim1  37354  naim2  37355  waj-ax  37379  lukshef-ax2  37380  ttctr  37458  dfttc2g  37471  bj-exim  37686  bj-sbievw1  37934  wl-dfcleq  38628  poimirlem26  38755  poimirlem30  38759  poimirlem32  38761  itg2addnclem  38780  ismtybndlem  38931  ablo4pnp  39005  isdrngo3  39084  keridl  39157  ispridl2  39163  ispridlc  39195  trcoss  39695  funALTVss  39907  disjss  39954  eldisjss  39961  prter1  40127  lshpdisj  40235  snatpsubN  40998  pmapglb2N  41019  pmapglb2xN  41020  elpaddn0  41048  sn-sup2  43746  mzpindd  43948  pellexlem3  44029  pellexlem5  44031  pellex  44033  2nn0ind  44143  lnr2i  44308  ofoaid1  44550  ofoaid2  44551  intabssd  44710  iunrelexpuztr  44909  hess  44970  frege52aid  45048  frege52b  45079  neik0pk1imk0  45237  relpmin  46135  rankrelp  46143  n0nsn2el  48298  imasetpreimafvbijlemfv1  48688  isubgredg  49167  stgrusgra  49260  isubgr3stgrlem6  49272  iinfsubc  50375  elsetrecslem  51070