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  1443  3orim123d  1444  sbi1  2071  moim  2547  mo3  2567  2euswapv  2633  2euswap  2648  exists2  2665  nelcon3d  3056  ral2imi  3091  ralimdv2  3169  reximdv2  3170  reximd2a  3275  moeq3  3734  rmoim  3762  2reuswap  3768  2reuswap2  3769  2rmoswap  3783  ssel  4002  sstr2OLD  4016  ssrexf  4075  ssrmof  4076  ssralv  4077  ssrexv  4078  ss2abdv  4089  rabss3d  4104  sscon  4166  ssdif  4167  unss1  4208  ssrin  4263  difin0ss  4396  r19.2z  4518  sspw  4633  uniss  4939  ssuni  4956  intssuni  4994  iinssiun  5028  iunss1  5029  iinss1  5030  ss2iun  5033  iunxdif3  5118  disjss2  5136  disjss1  5139  disjss3  5165  ssbrd  5209  poss  5609  pofun  5626  soss  5628  frss  5664  sess1  5665  sess2  5666  wess  5686  relss  5805  ssrel2  5809  ssrelrel  5820  relop  5875  dmss  5927  dmcosseq  5999  dmcosseqOLD  6000  funss  6597  fss  6763  fun  6783  brprcneu  6910  brprcneuALT  6911  f1eqcocnv  7337  isores3  7371  isomin  7373  isopolem  7381  isosolem  7383  isowe2  7386  ovmpos  7598  dfwe2  7809  epweon  7810  onint  7826  orduniorsuc  7866  trom  7912  finds  7936  finds2  7938  f1oweALT  8013  tposfn2  8289  tposfo2  8290  tposf1o2  8293  fprlem2  8342  smores  8408  tz7.48lem  8497  tz7.48-3  8500  oaass  8617  brinxper  8792  iiner  8847  xpdom2  9133  ssenen  9217  pssnn  9234  hartogs  9613  card2on  9623  ackbij1  10306  cfub  10318  fin23lem27  10397  fin1a2lem11  10479  fin1a2lem13  10481  hsmexlem2  10496  zorn2lem4  10568  ondomon  10632  gchina  10768  intgru  10883  ingru  10884  addclprlem2  11086  psslinpr  11100  ltexprlem3  11107  ltexprlem4  11108  reclem2pr  11117  suplem1pr  11121  sup2  12251  nnind  12311  nnunb  12549  uzind  12735  xmullem2  13327  xrsupsslem  13369  xrinfmsslem  13370  seqof  14110  hashfacen  14503  sswrd  14570  wrdind  14770  wrd2ind  14771  pfxccatin12lem2  14779  cau3lem  15403  caubnd  15407  sumodd  16436  vdwnnlem2  17043  ramub2  17061  fthres2  17999  odupos  18398  cycsubm  19242  lsmdisj2  19724  gsumxp2  20022  pgpfac1lem3  20121  nrhmzr  20563  subrgdvds  20614  lspdisj  21150  lspprat  21178  lbsextlem2  21184  ocv2ss  21714  ocvin  21715  coe1fzgsumd  22329  evl1gsumd  22382  tgcl  22997  epttop  23037  cmpsub  23429  tgcmp  23430  hauscmplem  23435  dfconn2  23448  llyss  23508  nllyss  23509  locfincmp  23555  txcnpi  23637  txcnp  23649  snfil  23893  fgcl  23907  filconn  23912  filuni  23914  cfinfil  23922  csdfil  23923  supfil  23924  ufildom1  23955  fin1aufil  23961  fmfnfmlem3  23985  ptcmplem2  24082  cldsubg  24140  iscau3  25331  iscau4  25332  caussi  25350  volfiniun  25601  plycj  26337  abelth  26503  wilthlem2  27130  lgsdir2lem4  27390  gausslemma2dlem0i  27426  gausslemma2dlem1a  27427  pntleml  27673  sltres  27725  nosupno  27766  noinfno  27781  nocvxmin  27841  noseqinds  28317  uhgr0vsize0  29274  cusgrfilem2  29492  uhgrvd00  29570  clwwisshclwws  30047  frcond3  30301  frgrncvvdeqlem2  30332  lpni  30512  ubthlem1  30902  chintcli  31363  h1de2i  31585  spansnm0i  31682  strlem1  32282  mdslmd1i  32361  reuxfrdf  32519  n0nsnel  32544  disjss1f  32594  disjpreima  32606  ssrelf  32637  suppss3  32738  nnindf  32823  wrdt2ind  32920  oduprs  32937  crefss  33795  esumpcvgval  34042  cbvex1v  35050  subgrtrl  35101  subgrpth  35102  subgrcycl  35103  derangenlem  35139  connpconn  35203  cvmsss2  35242  pocnv  35725  wzel  35788  in-ax8  36190  naim1  36355  naim2  36356  waj-ax  36380  lukshef-ax2  36381  bj-eximALT  36607  bj-sbievw1  36811  poimirlem26  37606  poimirlem30  37610  poimirlem32  37612  itg2addnclem  37631  ismtybndlem  37766  ablo4pnp  37840  isdrngo3  37919  keridl  37992  ispridl2  37998  ispridlc  38030  trcoss  38438  funALTVss  38655  disjss  38687  eldisjss  38694  prter1  38835  lshpdisj  38943  snatpsubN  39707  pmapglb2N  39728  pmapglb2xN  39729  elpaddn0  39757  ss2ab1  42212  sn-sup2  42447  nna4b4nsq  42615  mzpindd  42702  pellexlem3  42787  pellexlem5  42789  pellex  42791  2nn0ind  42902  lnr2i  43073  ofoaid1  43320  ofoaid2  43321  intabssd  43481  iunrelexpuztr  43681  hess  43742  frege52aid  43820  frege52b  43851  neik0pk1imk0  44009  n0nsn2el  46940  imasetpreimafvbijlemfv1  47277  elsetrecslem  48791