Theorem 3imtr4g 296

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  3anim123d  1445  3orim123d  1446  sbi1  2074  moim  2539  mo3  2559  2euswapv  2625  2euswap  2640  exists2  2657  nelcon3d  3036  ral2imi  3071  ralimdv2  3141  reximdv2  3142  reximd2a  3242  moeq3  3666  rmoim  3694  2reuswap  3700  2reuswap2  3701  2rmoswap  3715  ssel  3923  sstr2OLD  3937  ssrexf  3996  ssrmof  3997  ssralv  3998  ssrexv  3999  ss2abdv  4012  rabss3d  4028  sscon  4090  ssdif  4091  unss1  4132  ssrin  4189  difin0ss  4320  r19.2z  4442  sspw  4558  uniss  4864  ssuni  4881  intssuni  4918  iinssiun  4953  iunss1  4954  iinss1  4955  ss2iun  4958  iunxdif3  5041  disjss2  5059  disjss1  5062  disjss3  5088  ssbrd  5132  poss  5524  pofun  5540  soss  5542  frss  5578  sess1  5579  sess2  5580  wess  5600  relss  5721  ssrel2  5724  ssrelrel  5735  relop  5789  dmss  5841  dmcosseq  5916  dmcosseqOLD  5917  dmcosseqOLDOLD  5918  funss  6500  f1imadifssran  6567  fss  6667  fun  6685  brprcneu  6812  brprcneuALT  6813  f1eqcocnv  7235  isores3  7269  isomin  7271  isopolem  7279  isosolem  7281  isowe2  7284  ovmpos  7494  dfwe2  7707  epweon  7708  onint  7723  orduniorsuc  7760  trom  7805  finds  7826  finds2  7828  f1oweALT  7904  tposfn2  8178  tposfo2  8179  tposf1o2  8182  fprlem2  8231  smores  8272  tz7.48lem  8360  tz7.48-3  8363  oaass  8476  brinxper  8651  iiner  8713  xpdom2  8985  ssenen  9064  pssnn  9078  hartogs  9430  card2on  9440  ackbij1  10128  cfub  10140  fin23lem27  10219  fin1a2lem11  10301  fin1a2lem13  10303  hsmexlem2  10318  zorn2lem4  10390  ondomon  10454  gchina  10590  intgru  10705  ingru  10706  addclprlem2  10908  psslinpr  10922  ltexprlem3  10929  ltexprlem4  10930  reclem2pr  10939  suplem1pr  10943  sup2  12078  nnind  12143  nnunb  12377  uzind  12565  xmullem2  13164  xrsupsslem  13206  xrinfmsslem  13207  seqof  13966  hashfacen  14361  sswrd  14429  wrdind  14629  wrd2ind  14630  pfxccatin12lem2  14638  cau3lem  15262  caubnd  15266  sumodd  16299  vdwnnlem2  16908  ramub2  16926  fthres2  17841  oduprs  18206  odupos  18232  chnrss  18521  chndss  18522  cycsubm  19114  lsmdisj2  19594  gsumxp2  19892  pgpfac1lem3  19991  nrhmzr  20452  subrgdvds  20501  lspdisj  21062  lspprat  21090  lbsextlem2  21096  ocv2ss  21610  ocvin  21611  coe1fzgsumd  22219  evl1gsumd  22272  tgcl  22884  epttop  22924  cmpsub  23315  tgcmp  23316  hauscmplem  23321  dfconn2  23334  llyss  23394  nllyss  23395  locfincmp  23441  txcnpi  23523  txcnp  23535  snfil  23779  fgcl  23793  filconn  23798  filuni  23800  cfinfil  23808  csdfil  23809  supfil  23810  ufildom1  23841  fin1aufil  23847  fmfnfmlem3  23871  ptcmplem2  23968  cldsubg  24026  iscau3  25205  iscau4  25206  caussi  25224  volfiniun  25475  plycj  26210  plycjOLD  26212  abelth  26378  wilthlem2  27006  lgsdir2lem4  27266  gausslemma2dlem0i  27302  gausslemma2dlem1a  27303  pntleml  27549  sltres  27601  nosupno  27642  noinfno  27657  noseqinds  28223  uhgr0vsize0  29217  cusgrfilem2  29435  uhgrvd00  29513  clwwisshclwws  29995  frcond3  30249  frgrncvvdeqlem2  30280  lpni  30460  ubthlem1  30850  chintcli  31311  h1de2i  31533  spansnm0i  31630  strlem1  32230  mdslmd1i  32309  reuxfrdf  32470  n0nsnel  32495  disjss1f  32552  disjpreima  32564  ssrelf  32598  suppss3  32706  nnindf  32802  wrdt2ind  32934  crefss  33862  esumpcvgval  34091  cbvex1v  35086  r1filim  35115  onvf1odlem4  35150  subgrtrl  35177  subgrpth  35178  subgrcycl  35179  derangenlem  35215  connpconn  35279  cvmsss2  35318  pocnv  35807  wzel  35866  in-ax8  36268  naim1  36433  naim2  36434  waj-ax  36458  lukshef-ax2  36459  bj-eximALT  36685  bj-sbievw1  36889  poimirlem26  37685  poimirlem30  37689  poimirlem32  37691  itg2addnclem  37710  ismtybndlem  37845  ablo4pnp  37919  isdrngo3  37998  keridl  38071  ispridl2  38077  ispridlc  38109  trcoss  38583  funALTVss  38796  disjss  38828  eldisjss  38835  prter1  38977  lshpdisj  39085  snatpsubN  39848  pmapglb2N  39869  pmapglb2xN  39870  elpaddn0  39898  ss2ab1  42311  sn-sup2  42583  nna4b4nsq  42752  mzpindd  42838  pellexlem3  42923  pellexlem5  42925  pellex  42927  2nn0ind  43037  lnr2i  43208  ofoaid1  43450  ofoaid2  43451  intabssd  43611  iunrelexpuztr  43811  hess  43872  frege52aid  43950  frege52b  43981  neik0pk1imk0  44139  relpmin  45044  rankrelp  45052  n0nsn2el  47124  imasetpreimafvbijlemfv1  47502  isubgredg  47965  stgrusgra  48058  isubgr3stgrlem6  48070  iinfsubc  49158  elsetrecslem  49799