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	biimtrid 241	. 2 ⊢ (𝜑 → (𝜃 → 𝜒))
4		3imtr4g.3	. 2 ⊢ (𝜏 ↔ 𝜒)
5	3, 4	imbitrrdi 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  2072  moim  2536  mo3  2556  2euswapv  2624  2euswap  2639  exists2  2655  nelcon3d  3048  ral2imi  3083  ralimdv2  3161  reximdv2  3162  reximd2a  3264  moeq3  3707  rmoim  3735  2reuswap  3741  2reuswap2  3742  2rmoswap  3756  ssel  3974  sselOLD  3975  sstr2  3988  ssrexf  4047  ssrmof  4048  ss2abdvALT  4060  rabss3d  4078  sscon  4137  ssdif  4138  unss1  4178  ssrin  4232  difin0ss  4367  r19.2z  4493  sspw  4612  uniss  4915  ssuni  4935  intssuni  4973  iinssiun  5009  iunss1  5010  iinss1  5011  ss2iun  5014  iunxdif3  5097  disjss2  5115  disjss1  5118  disjss3  5146  ssbrd  5190  poss  5589  pofun  5605  soss  5607  frss  5642  sess1  5643  sess2  5644  wess  5662  relss  5780  ssrel2  5784  ssrelrel  5795  relop  5849  dmss  5901  dmcosseq  5971  funss  6566  fss  6733  fun  6752  brprcneu  6880  brprcneuALT  6881  f1eqcocnv  7301  f1eqcocnvOLD  7302  isores3  7334  isomin  7336  isopolem  7344  isosolem  7346  isowe2  7349  ovmpos  7558  dfwe2  7763  epweon  7764  onint  7780  orduniorsuc  7820  trom  7866  finds  7891  finds2  7893  f1oweALT  7961  tposfn2  8235  tposfo2  8236  tposf1o2  8239  fprlem2  8288  smores  8354  tz7.48lem  8443  tz7.48-3  8446  oaass  8563  iiner  8785  xpdom2  9069  ssenen  9153  pssnn  9170  pssnnOLD  9267  hartogs  9541  card2on  9551  ackbij1  10235  cfub  10246  fin23lem27  10325  fin1a2lem11  10407  fin1a2lem13  10409  hsmexlem2  10424  zorn2lem4  10496  ondomon  10560  gchina  10696  intgru  10811  ingru  10812  addclprlem2  11014  psslinpr  11028  ltexprlem3  11035  ltexprlem4  11036  reclem2pr  11045  suplem1pr  11049  sup2  12174  nnind  12234  nnunb  12472  uzind  12658  xmullem2  13248  xrsupsslem  13290  xrinfmsslem  13291  seqof  14029  hashfacen  14417  hashfacenOLD  14418  sswrd  14476  wrdind  14676  wrd2ind  14677  pfxccatin12lem2  14685  cau3lem  15305  caubnd  15309  sumodd  16335  vdwnnlem2  16933  ramub2  16951  fthres2  17887  odupos  18285  cycsubm  19117  lsmdisj2  19591  gsumxp2  19889  pgpfac1lem3  19988  subrgdvds  20476  lspdisj  20883  lspprat  20911  lbsextlem2  20917  ocv2ss  21445  ocvin  21446  coe1fzgsumd  22046  evl1gsumd  22096  tgcl  22692  epttop  22732  cmpsub  23124  tgcmp  23125  hauscmplem  23130  dfconn2  23143  llyss  23203  nllyss  23204  locfincmp  23250  txcnpi  23332  txcnp  23344  snfil  23588  fgcl  23602  filconn  23607  filuni  23609  cfinfil  23617  csdfil  23618  supfil  23619  ufildom1  23650  fin1aufil  23656  fmfnfmlem3  23680  ptcmplem2  23777  cldsubg  23835  iscau3  25026  iscau4  25027  caussi  25045  volfiniun  25296  plycj  26027  abelth  26189  wilthlem2  26809  lgsdir2lem4  27067  gausslemma2dlem0i  27103  gausslemma2dlem1a  27104  pntleml  27350  sltres  27401  nosupno  27442  noinfno  27457  nocvxmin  27516  uhgr0vsize0  28763  cusgrfilem2  28980  uhgrvd00  29058  clwwisshclwws  29535  frcond3  29789  frgrncvvdeqlem2  29820  lpni  30000  ubthlem1  30390  chintcli  30851  h1de2i  31073  spansnm0i  31170  strlem1  31770  mdslmd1i  31849  reuxfrdf  31998  disjss1f  32070  disjpreima  32082  ssrelf  32111  suppss3  32216  nnindf  32292  wrdt2ind  32384  oduprs  32401  crefss  33127  esumpcvgval  33374  subgrtrl  34422  subgrpth  34423  subgrcycl  34424  derangenlem  34460  connpconn  34524  cvmsss2  34563  pocnv  35037  wzel  35100  naim1  35577  naim2  35578  waj-ax  35602  lukshef-ax2  35603  bj-eximALT  35821  bj-sbievw1  36027  poimirlem26  36817  poimirlem30  36821  poimirlem32  36823  itg2addnclem  36842  ismtybndlem  36977  ablo4pnp  37051  isdrngo3  37130  keridl  37203  ispridl2  37209  ispridlc  37241  trcoss  37655  funALTVss  37872  disjss  37904  eldisjss  37911  prter1  38052  lshpdisj  38160  snatpsubN  38924  pmapglb2N  38945  pmapglb2xN  38946  elpaddn0  38974  ss2ab1  41342  sn-sup2  41644  nna4b4nsq  41704  mzpindd  41786  pellexlem3  41871  pellexlem5  41873  pellex  41875  2nn0ind  41986  lnr2i  42160  ofoaid1  42410  ofoaid2  42411  intabssd  42572  iunrelexpuztr  42772  hess  42833  frege52aid  42911  frege52b  42942  neik0pk1imk0  43100  n0nsn2el  46033  imasetpreimafvbijlemfv1  46369  nrhmzr  46910  elsetrecslem  47831