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	syl5bi 245	. 2 ⊢ (𝜑 → (𝜃 → 𝜒))
4		3imtr4g.3	. 2 ⊢ (𝜏 ↔ 𝜒)
5	3, 4	syl6ibr 255	1 ⊢ (𝜑 → (𝜃 → 𝜏))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  3anim123d  1440  3orim123d  1441  sbi1  2076  moim  2602  mo3  2623  2euswapv  2692  2euswap  2707  exists2  2724  nelcon3d  3103  ral2imi  3124  ralimdv2  3143  rexim  3204  reximdv2  3230  reximd2a  3271  moeq3  3651  rmoim  3679  2reuswap  3685  2reuswap2  3686  2rmoswap  3700  ssel  3908  sselOLD  3909  sstr2  3922  ssrexf  3979  ssrmof  3980  ss2abdvALT  3992  sscon  4066  ssdif  4067  unss1  4106  ssrin  4160  difin0ss  4282  r19.2z  4398  sspw  4510  uniss  4808  ssuni  4825  intssuni  4860  iinssiun  4894  iunss1  4895  iinss1  4896  ss2iun  4899  iunxdif3  4980  disjss2  4998  disjss1  5001  disjss3  5029  ssbrd  5073  poss  5440  pofun  5455  soss  5457  frss  5486  sess1  5487  sess2  5488  wess  5506  relss  5620  ssrel2  5623  ssrelrel  5633  relop  5685  dmss  5735  dmcosseq  5809  funss  6343  fss  6501  fun  6514  brprcneu  6637  f1eqcocnv  7035  f1eqcocnvOLD  7036  isores3  7067  isomin  7069  isopolem  7077  isosolem  7079  isowe2  7082  ovmpos  7277  dfwe2  7476  onint  7490  orduniorsuc  7525  ordom  7569  finds  7589  finds2  7591  f1oweALT  7655  tposfn2  7897  tposfo2  7898  tposf1o2  7901  smores  7972  tz7.48lem  8060  tz7.48-3  8063  oaass  8170  iiner  8352  xpdom2  8595  ssenen  8675  pssnn  8720  hartogs  8992  card2on  9002  ackbij1  9649  cfub  9660  fin23lem27  9739  fin1a2lem11  9821  fin1a2lem13  9823  hsmexlem2  9838  zorn2lem4  9910  ondomon  9974  gchina  10110  intgru  10225  ingru  10226  addclprlem2  10428  psslinpr  10442  ltexprlem3  10449  ltexprlem4  10450  reclem2pr  10459  suplem1pr  10463  sup2  11584  nnind  11643  nnunb  11881  uzind  12062  xmullem2  12646  xrsupsslem  12688  xrinfmsslem  12689  seqof  13423  hashfacen  13808  sswrd  13865  wrdind  14075  wrd2ind  14076  pfxccatin12lem2  14084  cau3lem  14706  caubnd  14710  sumodd  15729  vdwnnlem2  16322  ramub2  16340  fthres2  17194  odupos  17737  cycsubm  18337  lsmdisj2  18800  gsumxp2  19093  pgpfac1lem3  19192  subrgdvds  19542  lspdisj  19890  lspprat  19918  lbsextlem2  19924  ocv2ss  20362  ocvin  20363  coe1fzgsumd  20931  evl1gsumd  20981  tgcl  21574  epttop  21614  cmpsub  22005  tgcmp  22006  hauscmplem  22011  dfconn2  22024  llyss  22084  nllyss  22085  locfincmp  22131  txcnpi  22213  txcnp  22225  snfil  22469  fgcl  22483  filconn  22488  filuni  22490  cfinfil  22498  csdfil  22499  supfil  22500  ufildom1  22531  fin1aufil  22537  fmfnfmlem3  22561  ptcmplem2  22658  cldsubg  22716  iscau3  23882  iscau4  23883  caussi  23901  volfiniun  24151  plycj  24874  abelth  25036  wilthlem2  25654  lgsdir2lem4  25912  gausslemma2dlem0i  25948  gausslemma2dlem1a  25949  pntleml  26195  uhgr0vsize0  27029  cusgrfilem2  27246  uhgrvd00  27324  clwwisshclwws  27800  frcond3  28054  frgrncvvdeqlem2  28085  lpni  28263  ubthlem1  28653  chintcli  29114  h1de2i  29336  spansnm0i  29433  strlem1  30033  mdslmd1i  30112  reuxfrdf  30262  rabss3d  30285  disjss1f  30335  disjpreima  30347  ssrelf  30379  suppss3  30486  nnindf  30561  wrdt2ind  30653  oduprs  30669  crefss  31202  esumpcvgval  31447  subgrtrl  32493  subgrpth  32494  subgrcycl  32495  derangenlem  32531  connpconn  32595  cvmsss2  32634  pocnv  33112  wzel  33224  fprlem2  33251  sltres  33282  nosupno  33316  nocvxmin  33361  naim1  33850  naim2  33851  waj-ax  33875  lukshef-ax2  33876  bj-eximALT  34087  bj-sbievw1  34284  poimirlem26  35083  poimirlem30  35087  poimirlem32  35089  itg2addnclem  35108  ismtybndlem  35244  ablo4pnp  35318  isdrngo3  35397  keridl  35470  ispridl2  35476  ispridlc  35508  trcoss  35882  funALTVss  36092  disjss  36124  eldisjss  36131  prter1  36175  lshpdisj  36283  snatpsubN  37046  pmapglb2N  37067  pmapglb2xN  37068  elpaddn0  37096  sn-sup2  39594  mzpindd  39687  pellexlem3  39772  pellexlem5  39774  pellex  39776  2nn0ind  39886  lnr2i  40060  intabssd  40227  iunrelexpuztr  40420  hess  40481  frege52aid  40559  frege52b  40590  neik0pk1imk0  40750  imasetpreimafvbijlemfv1  43920  nrhmzr  44497  elsetrecslem  45228