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  1444  3orim123d  1445  sbi1  2081  moim  2545  mo3  2565  2euswapv  2634  2euswap  2649  exists2  2665  nelcon3d  3051  ral2imi  3072  ralimdv2  3091  rexim  3155  reximdv2  3182  reximd2a  3223  moeq3  3612  rmoim  3640  2reuswap  3646  2reuswap2  3647  2rmoswap  3661  ssel  3871  sselOLD  3872  sstr2  3885  ssrexf  3942  ssrmof  3943  ss2abdvALT  3955  sscon  4030  ssdif  4031  unss1  4070  ssrin  4125  difin0ss  4258  r19.2z  4382  sspw  4502  uniss  4805  ssuni  4824  intssuni  4859  iinssiun  4895  iunss1  4896  iinss1  4897  ss2iun  4900  iunxdif3  4981  disjss2  4999  disjss1  5002  disjss3  5030  ssbrd  5074  poss  5445  pofun  5461  soss  5463  frss  5493  sess1  5494  sess2  5495  wess  5513  relss  5628  ssrel2  5631  ssrelrel  5641  relop  5694  dmss  5746  dmcosseq  5817  funss  6359  fss  6522  fun  6541  brprcneu  6668  fvprc  6669  f1eqcocnv  7071  f1eqcocnvOLD  7072  isores3  7104  isomin  7106  isopolem  7114  isosolem  7116  isowe2  7119  ovmpos  7316  dfwe2  7518  onint  7532  orduniorsuc  7567  ordom  7611  finds  7632  finds2  7634  f1oweALT  7701  tposfn2  7946  tposfo2  7947  tposf1o2  7950  smores  8021  tz7.48lem  8109  tz7.48-3  8112  oaass  8221  iiner  8403  xpdom2  8664  ssenen  8744  pssnn  8770  pssnnOLD  8818  hartogs  9084  card2on  9094  ackbij1  9741  cfub  9752  fin23lem27  9831  fin1a2lem11  9913  fin1a2lem13  9915  hsmexlem2  9930  zorn2lem4  10002  ondomon  10066  gchina  10202  intgru  10317  ingru  10318  addclprlem2  10520  psslinpr  10534  ltexprlem3  10541  ltexprlem4  10542  reclem2pr  10551  suplem1pr  10555  sup2  11677  nnind  11737  nnunb  11975  uzind  12158  xmullem2  12744  xrsupsslem  12786  xrinfmsslem  12787  seqof  13522  hashfacen  13907  hashfacenOLD  13908  sswrd  13966  wrdind  14176  wrd2ind  14177  pfxccatin12lem2  14185  cau3lem  14807  caubnd  14811  sumodd  15836  vdwnnlem2  16435  ramub2  16453  fthres2  17310  odupos  17864  cycsubm  18466  lsmdisj2  18929  gsumxp2  19222  pgpfac1lem3  19321  subrgdvds  19671  lspdisj  20019  lspprat  20047  lbsextlem2  20053  ocv2ss  20492  ocvin  20493  coe1fzgsumd  21080  evl1gsumd  21130  tgcl  21723  epttop  21763  cmpsub  22154  tgcmp  22155  hauscmplem  22160  dfconn2  22173  llyss  22233  nllyss  22234  locfincmp  22280  txcnpi  22362  txcnp  22374  snfil  22618  fgcl  22632  filconn  22637  filuni  22639  cfinfil  22647  csdfil  22648  supfil  22649  ufildom1  22680  fin1aufil  22686  fmfnfmlem3  22710  ptcmplem2  22807  cldsubg  22865  iscau3  24033  iscau4  24034  caussi  24052  volfiniun  24302  plycj  25029  abelth  25191  wilthlem2  25809  lgsdir2lem4  26067  gausslemma2dlem0i  26103  gausslemma2dlem1a  26104  pntleml  26350  uhgr0vsize0  27184  cusgrfilem2  27401  uhgrvd00  27479  clwwisshclwws  27955  frcond3  28209  frgrncvvdeqlem2  28240  lpni  28418  ubthlem1  28808  chintcli  29269  h1de2i  29491  spansnm0i  29588  strlem1  30188  mdslmd1i  30267  reuxfrdf  30416  rabss3d  30438  disjss1f  30488  disjpreima  30500  ssrelf  30532  suppss3  30637  nnindf  30711  wrdt2ind  30803  oduprs  30819  crefss  31374  esumpcvgval  31619  subgrtrl  32669  subgrpth  32670  subgrcycl  32671  derangenlem  32707  connpconn  32771  cvmsss2  32810  pocnv  33307  wzel  33434  fprlem2  33461  sltres  33511  nosupno  33552  noinfno  33567  nocvxmin  33619  naim1  34224  naim2  34225  waj-ax  34249  lukshef-ax2  34250  bj-eximALT  34468  bj-sbievw1  34675  poimirlem26  35449  poimirlem30  35453  poimirlem32  35455  itg2addnclem  35474  ismtybndlem  35610  ablo4pnp  35684  isdrngo3  35763  keridl  35836  ispridl2  35842  ispridlc  35874  trcoss  36246  funALTVss  36456  disjss  36488  eldisjss  36495  prter1  36539  lshpdisj  36647  snatpsubN  37410  pmapglb2N  37431  pmapglb2xN  37432  elpaddn0  37460  sn-sup2  40039  nna4b4nsq  40092  mzpindd  40163  pellexlem3  40248  pellexlem5  40250  pellex  40252  2nn0ind  40362  lnr2i  40536  intabssd  40703  iunrelexpuztr  40896  hess  40957  frege52aid  41035  frege52b  41066  neik0pk1imk0  41226  imasetpreimafvbijlemfv1  44419  nrhmzr  44995  elsetrecslem  45887