Theorem 3imtr4g 295

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  3anim123d  1441  3orim123d  1442  sbi1  2075  moim  2544  mo3  2564  2euswapv  2632  2euswap  2647  exists2  2663  nelcon3d  3060  ral2imi  3081  ralimdv2  3101  rexim  3168  reximdv2  3198  reximd2a  3240  moeq3  3642  rmoim  3670  2reuswap  3676  2reuswap2  3677  2rmoswap  3691  ssel  3910  sselOLD  3911  sstr2  3924  ssrexf  3981  ssrmof  3982  ss2abdvALT  3994  sscon  4069  ssdif  4070  unss1  4109  ssrin  4164  difin0ss  4299  r19.2z  4422  sspw  4543  uniss  4844  ssuni  4863  intssuni  4898  iinssiun  4934  iunss1  4935  iinss1  4936  ss2iun  4939  iunxdif3  5020  disjss2  5038  disjss1  5041  disjss3  5069  ssbrd  5113  poss  5496  pofun  5512  soss  5514  frss  5547  sess1  5548  sess2  5549  wess  5567  relss  5682  ssrel2  5685  ssrelrel  5695  relop  5748  dmss  5800  dmcosseq  5871  funss  6437  fss  6601  fun  6620  brprcneu  6747  fvprc  6748  f1eqcocnv  7153  f1eqcocnvOLD  7154  isores3  7186  isomin  7188  isopolem  7196  isosolem  7198  isowe2  7201  ovmpos  7399  dfwe2  7602  onint  7617  orduniorsuc  7652  trom  7696  finds  7719  finds2  7721  f1oweALT  7788  tposfn2  8035  tposfo2  8036  tposf1o2  8039  fprlem2  8088  smores  8154  tz7.48lem  8242  tz7.48-3  8245  oaass  8354  iiner  8536  xpdom2  8807  ssenen  8887  pssnn  8913  pssnnOLD  8969  hartogs  9233  card2on  9243  ackbij1  9925  cfub  9936  fin23lem27  10015  fin1a2lem11  10097  fin1a2lem13  10099  hsmexlem2  10114  zorn2lem4  10186  ondomon  10250  gchina  10386  intgru  10501  ingru  10502  addclprlem2  10704  psslinpr  10718  ltexprlem3  10725  ltexprlem4  10726  reclem2pr  10735  suplem1pr  10739  sup2  11861  nnind  11921  nnunb  12159  uzind  12342  xmullem2  12928  xrsupsslem  12970  xrinfmsslem  12971  seqof  13708  hashfacen  14094  hashfacenOLD  14095  sswrd  14153  wrdind  14363  wrd2ind  14364  pfxccatin12lem2  14372  cau3lem  14994  caubnd  14998  sumodd  16025  vdwnnlem2  16625  ramub2  16643  fthres2  17564  odupos  17961  cycsubm  18736  lsmdisj2  19203  gsumxp2  19496  pgpfac1lem3  19595  subrgdvds  19953  lspdisj  20302  lspprat  20330  lbsextlem2  20336  ocv2ss  20790  ocvin  20791  coe1fzgsumd  21383  evl1gsumd  21433  tgcl  22027  epttop  22067  cmpsub  22459  tgcmp  22460  hauscmplem  22465  dfconn2  22478  llyss  22538  nllyss  22539  locfincmp  22585  txcnpi  22667  txcnp  22679  snfil  22923  fgcl  22937  filconn  22942  filuni  22944  cfinfil  22952  csdfil  22953  supfil  22954  ufildom1  22985  fin1aufil  22991  fmfnfmlem3  23015  ptcmplem2  23112  cldsubg  23170  iscau3  24347  iscau4  24348  caussi  24366  volfiniun  24616  plycj  25343  abelth  25505  wilthlem2  26123  lgsdir2lem4  26381  gausslemma2dlem0i  26417  gausslemma2dlem1a  26418  pntleml  26664  uhgr0vsize0  27509  cusgrfilem2  27726  uhgrvd00  27804  clwwisshclwws  28280  frcond3  28534  frgrncvvdeqlem2  28565  lpni  28743  ubthlem1  29133  chintcli  29594  h1de2i  29816  spansnm0i  29913  strlem1  30513  mdslmd1i  30592  reuxfrdf  30740  rabss3d  30762  disjss1f  30812  disjpreima  30824  ssrelf  30856  suppss3  30961  nnindf  31035  wrdt2ind  31127  oduprs  31144  crefss  31701  esumpcvgval  31946  subgrtrl  32995  subgrpth  32996  subgrcycl  32997  derangenlem  33033  connpconn  33097  cvmsss2  33136  pocnv  33636  wzel  33745  sltres  33792  nosupno  33833  noinfno  33848  nocvxmin  33900  naim1  34505  naim2  34506  waj-ax  34530  lukshef-ax2  34531  bj-eximALT  34749  bj-sbievw1  34956  poimirlem26  35730  poimirlem30  35734  poimirlem32  35736  itg2addnclem  35755  ismtybndlem  35891  ablo4pnp  35965  isdrngo3  36044  keridl  36117  ispridl2  36123  ispridlc  36155  trcoss  36527  funALTVss  36737  disjss  36769  eldisjss  36776  prter1  36820  lshpdisj  36928  snatpsubN  37691  pmapglb2N  37712  pmapglb2xN  37713  elpaddn0  37741  sn-sup2  40360  nna4b4nsq  40413  mzpindd  40484  pellexlem3  40569  pellexlem5  40571  pellex  40573  2nn0ind  40683  lnr2i  40857  intabssd  41024  iunrelexpuztr  41216  hess  41277  frege52aid  41355  frege52b  41386  neik0pk1imk0  41546  imasetpreimafvbijlemfv1  44743  nrhmzr  45319  elsetrecslem  46290