Theorem 3imtr4g 298

Description: More general version of 3imtr4i 294. 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	syl5bi 244	. 2 ⊢ (𝜑 → (𝜃 → 𝜒))
4		3imtr4g.3	. 2 ⊢ (𝜏 ↔ 𝜒)
5	3, 4	syl6ibr 254	1 ⊢ (𝜑 → (𝜃 → 𝜏))

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  3anim123d  1439  3orim123d  1440  sbi1  2076  sbequivvOLD  2334  sbimdvOLD  2516  sbimdOLD  2518  moim  2626  mo3  2648  2euswapv  2715  2euswap  2730  exists2  2747  nelcon3d  3135  ral2imi  3156  ralimdv2  3176  rexim  3241  reximdv2  3271  reximd2a  3312  moeq3  3703  rmoim  3731  2reuswap  3737  2reuswap2  3738  2rmoswap  3752  ssel  3961  sstr2  3974  ssrexf  4031  ssrmof  4032  sscon  4115  ssdif  4116  unss1  4155  ssrin  4210  difin0ss  4328  r19.2z  4440  sspw  4552  uniss  4846  ssuni  4863  intssuni  4898  iinssiun  4932  iunss1  4933  iinss1  4934  ss2iun  4937  iunxdif3  5017  disjss2  5034  disjss1  5037  disjss3  5065  ssbrd  5109  poss  5476  pofun  5491  soss  5493  frss  5522  sess1  5523  sess2  5524  wess  5542  relss  5656  ssrel2  5659  ssrelrel  5669  relop  5721  dmss  5771  dmcosseq  5844  funss  6374  fss  6527  fun  6540  brprcneu  6662  f1eqcocnv  7057  isores3  7088  isomin  7090  isopolem  7098  isosolem  7100  isowe2  7103  ovmpos  7298  dfwe2  7496  onint  7510  orduniorsuc  7545  ordom  7589  finds  7608  finds2  7610  f1oweALT  7673  tposfn2  7914  tposfo2  7915  tposf1o2  7918  smores  7989  tz7.48lem  8077  tz7.48-3  8080  oaass  8187  iiner  8369  xpdom2  8612  ssenen  8691  pssnn  8736  hartogs  9008  card2on  9018  ackbij1  9660  cfub  9671  fin23lem27  9750  fin1a2lem11  9832  fin1a2lem13  9834  hsmexlem2  9849  zorn2lem4  9921  ondomon  9985  gchina  10121  intgru  10236  ingru  10237  addclprlem2  10439  psslinpr  10453  ltexprlem3  10460  ltexprlem4  10461  reclem2pr  10470  suplem1pr  10474  sup2  11597  nnind  11656  nnunb  11894  uzind  12075  xmullem2  12659  xrsupsslem  12701  xrinfmsslem  12702  seqof  13428  hashfacen  13813  sswrd  13870  wrdind  14084  wrd2ind  14085  pfxccatin12lem2  14093  cau3lem  14714  caubnd  14718  sumodd  15739  vdwnnlem2  16332  ramub2  16350  fthres2  17202  odupos  17745  cycsubm  18345  lsmdisj2  18808  gsumxp2  19100  pgpfac1lem3  19199  subrgdvds  19549  lspdisj  19897  lspprat  19925  lbsextlem2  19931  coe1fzgsumd  20470  evl1gsumd  20520  ocv2ss  20817  ocvin  20818  tgcl  21577  epttop  21617  cmpsub  22008  tgcmp  22009  hauscmplem  22014  dfconn2  22027  llyss  22087  nllyss  22088  locfincmp  22134  txcnpi  22216  txcnp  22228  snfil  22472  fgcl  22486  filconn  22491  filuni  22493  cfinfil  22501  csdfil  22502  supfil  22503  ufildom1  22534  fin1aufil  22540  fmfnfmlem3  22564  ptcmplem2  22661  cldsubg  22719  iscau3  23881  iscau4  23882  caussi  23900  volfiniun  24148  plycj  24867  abelth  25029  wilthlem2  25646  lgsdir2lem4  25904  gausslemma2dlem0i  25940  gausslemma2dlem1a  25941  pntleml  26187  uhgr0vsize0  27021  cusgrfilem2  27238  uhgrvd00  27316  clwwisshclwws  27793  frcond3  28048  frgrncvvdeqlem2  28079  lpni  28257  ubthlem1  28647  chintcli  29108  h1de2i  29330  spansnm0i  29427  strlem1  30027  mdslmd1i  30106  reuxfrdf  30255  rabss3d  30276  disjss1f  30322  disjpreima  30334  ssrelf  30366  suppss3  30460  nnindf  30535  wrdt2ind  30627  oduprs  30643  crefss  31113  esumpcvgval  31337  subgrtrl  32380  subgrpth  32381  subgrcycl  32382  derangenlem  32418  connpconn  32482  cvmsss2  32521  pocnv  32999  wzel  33111  fprlem2  33138  sltres  33169  nosupno  33203  nocvxmin  33248  naim1  33737  naim2  33738  waj-ax  33762  lukshef-ax2  33763  bj-eximALT  33974  bj-sbievw1  34169  poimirlem26  34933  poimirlem30  34937  poimirlem32  34939  itg2addnclem  34958  ismtybndlem  35099  ablo4pnp  35173  isdrngo3  35252  keridl  35325  ispridl2  35331  ispridlc  35363  trcoss  35737  funALTVss  35947  disjss  35979  eldisjss  35986  prter1  36030  lshpdisj  36138  snatpsubN  36901  pmapglb2N  36922  pmapglb2xN  36923  elpaddn0  36951  mzpindd  39363  pellexlem3  39448  pellexlem5  39450  pellex  39452  2nn0ind  39562  lnr2i  39736  intabssd  39905  iunrelexpuztr  40084  hess  40146  frege52aid  40224  frege52b  40255  neik0pk1imk0  40417  imasetpreimafvbijlemfv1  43583  ichan  43650  nrhmzr  44164  elsetrecslem  44821