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	biimtrid 245	. 2 ⊢ (𝜑 → (𝜃 → 𝜒))
4		3imtr4g.3	. 2 ⊢ (𝜏 ↔ 𝜒)
5	3, 4	imbitrrdi 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  1469  3orim123d  1470  sbi1ALT  2111  moim  2578  mo3  2598  2euswapv  2664  2euswap  2679  exists2  2695  nelcon3d  3074  ral2imi  3110  ralimdv2  3180  reximdv2  3181  reximd2a  3281  moeq3  3684  rmoim  3712  2reuswap  3718  2reuswap2  3719  2rmoswap  3733  ssel  3939  ssrexf  4012  ssrmof  4013  ssralv  4014  ssrexv  4015  ss2abim  4022  ss2abdv  4027  rabss3d  4043  sscon  4105  ssdif  4106  unss1  4146  ssrin  4202  difin0ss  4336  r19.2z  4465  sspw  4578  uniss  4884  ssuni  4902  intssuni  4939  iinssiun  4974  iunss1  4975  iinss1  4976  ss2iun  4979  iunxdif3  5065  disjss2  5083  disjss1  5086  disjss3  5112  ssbrd  5158  poss  5572  pofun  5588  soss  5590  frss  5626  sess1  5627  sess2  5628  wess  5648  relss  5769  ssrel2  5772  ssrelrel  5783  relop  5837  dmss  5893  dmcosseq  5969  dmcosseqOLD  5970  funss  6556  fss  6723  fun  6741  brprcneu  6872  brprcneuALT  6873  f1eqcocnv  7300  isores3  7334  isomin  7336  isopolem  7344  isosolem  7346  isowe2  7349  ovmpos  7559  dfwe2  7773  epweon  7774  onint  7789  orduniorsuc  7826  trom  7871  finds  7893  finds2  7895  f1oweALT  7969  tposfn2  8244  tposfo2  8245  tposf1o2  8248  fprlem2  8298  smores  8339  tz7.48lem  8428  tz7.48-3  8431  oaass  8546  brinxper  8724  iiner  8787  xpdom2  9060  ssenen  9139  pssnn  9153  hartogs  9506  card2on  9516  ackbij1  10220  cfub  10232  fin23lem27  10312  fin1a2lem11  10394  fin1a2lem13  10396  hsmexlem2  10411  zorn2lem4  10483  ondomon  10547  gchina  10684  intgru  10799  ingru  10800  addclprlem2  11002  psslinpr  11016  ltexprlem3  11023  ltexprlem4  11024  reclem2pr  11033  suplem1pr  11037  sup2  12171  nnind  12251  nnunb  12500  uzind  12688  xmullem2  13291  xrsupsslem  13333  xrinfmsslem  13334  seqof  14095  hashfacen  14491  sswrd  14559  wrdind  14759  wrd2ind  14760  pfxccatin12lem2  14768  cau3lem  15406  caubnd  15410  sumodd  16446  vdwnnlem2  17056  ramub2  17074  fthres2  17991  oduprs  18356  odupos  18382  chnrss  18671  chndss  18672  cycsubm  19273  lsmdisj2  19752  gsumxp2  20050  pgpfac1lem3  20149  nrhmzr  20622  subrgdvds  20671  lspdisj  21227  lspprat  21255  lbsextlem2  21261  ocv2ss  21792  ocvin  21793  coe1fzgsumd  22433  evl1gsumd  22486  tgcl  23095  epttop  23135  cmpsub  23526  tgcmp  23527  hauscmplem  23532  dfconn2  23545  llyss  23605  nllyss  23606  locfincmp  23652  txcnpi  23734  txcnp  23746  snfil  23990  fgcl  24004  filconn  24009  filuni  24011  cfinfil  24019  csdfil  24020  supfil  24021  ufildom1  24052  fin1aufil  24058  fmfnfmlem3  24082  ptcmplem2  24179  cldsubg  24237  iscau3  25406  iscau4  25407  caussi  25425  volfiniun  25675  plycj  26403  plycjOLD  26405  abelth  26570  wilthlem2  27199  lgsdir2lem4  27458  gausslemma2dlem0i  27494  gausslemma2dlem1a  27495  pntleml  27741  ltsres  27792  nosupno  27833  noinfno  27848  noseqinds  28452  plngrotlem2  29028  uhgr0vsize0  29530  cusgrfilem2  29747  uhgrvd00  29825  clwwisshclwws  30307  frcond3  30561  frgrncvvdeqlem2  30592  lpni  30773  ubthlem1  31163  chintcli  31624  h1de2i  31846  spansnm0i  31943  strlem1  32543  mdslmd1i  32622  reuxfrdf  32778  n0nsnel  32802  disjss1f  32858  disjpreima  32870  ssrelf  32901  suppss3  33009  nnindf  33105  wrdt2ind  33214  crefss  34184  esumpcvgval  34413  cbvex1v  35407  r1filim  35441  onvf1odlem4  35523  subgrtrl  35558  subgrpth  35559  subgrcycl  35560  derangenlem  35596  connpconn  35660  cvmsss2  35699  pocnv  36188  wzel  36247  in-ax8  36659  naim1  36823  naim2  36824  waj-ax  36848  lukshef-ax2  36849  ttctr  36927  dfttc2g  36940  bj-exim  37155  bj-sbievw1  37403  wl-dfcleq  38082  poimirlem26  38219  poimirlem30  38223  poimirlem32  38225  itg2addnclem  38244  ismtybndlem  38379  ablo4pnp  38453  isdrngo3  38532  keridl  38605  ispridl2  38611  ispridlc  38643  trcoss  39145  funALTVss  39357  disjss  39404  eldisjss  39411  prter1  39577  lshpdisj  39685  snatpsubN  40448  pmapglb2N  40469  pmapglb2xN  40470  elpaddn0  40498  sn-sup2  43189  nna4b4nsq  43318  mzpindd  43403  pellexlem3  43484  pellexlem5  43486  pellex  43488  2nn0ind  43598  lnr2i  43769  ofoaid1  44011  ofoaid2  44012  intabssd  44171  iunrelexpuztr  44371  hess  44432  frege52aid  44510  frege52b  44541  neik0pk1imk0  44699  relpmin  45587  rankrelp  45595  n0nsn2el  47685  imasetpreimafvbijlemfv1  48075  isubgredg  48554  stgrusgra  48647  isubgr3stgrlem6  48659  iinfsubc  49755  elsetrecslem  50396