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  1446  3orim123d  1447  sbi1  2077  moim  2545  mo3  2565  2euswapv  2631  2euswap  2646  exists2  2663  nelcon3d  3041  ral2imi  3077  ralimdv2  3147  reximdv2  3148  reximd2a  3248  moeq3  3659  rmoim  3687  2reuswap  3693  2reuswap2  3694  2rmoswap  3708  ssel  3916  sstr2OLD  3930  ssrexf  3989  ssrmof  3990  ssralv  3991  ssrexv  3992  ss2abim  4001  ss2abdv  4006  rabss3d  4022  sscon  4084  ssdif  4085  unss1  4126  ssrin  4183  difin0ss  4314  r19.2z  4440  sspw  4553  uniss  4859  ssuni  4876  intssuni  4913  iinssiun  4948  iunss1  4949  iinss1  4950  ss2iun  4953  iunxdif3  5038  disjss2  5056  disjss1  5059  disjss3  5085  ssbrd  5129  poss  5536  pofun  5552  soss  5554  frss  5590  sess1  5591  sess2  5592  wess  5612  relss  5733  ssrel2  5736  ssrelrel  5747  relop  5801  dmss  5853  dmcosseq  5929  dmcosseqOLD  5930  dmcosseqOLDOLD  5931  funss  6513  f1imadifssran  6580  fss  6680  fun  6698  brprcneu  6826  brprcneuALT  6827  f1eqcocnv  7251  isores3  7285  isomin  7287  isopolem  7295  isosolem  7297  isowe2  7300  ovmpos  7510  dfwe2  7723  epweon  7724  onint  7739  orduniorsuc  7776  trom  7821  finds  7842  finds2  7844  f1oweALT  7920  tposfn2  8193  tposfo2  8194  tposf1o2  8197  fprlem2  8246  smores  8287  tz7.48lem  8375  tz7.48-3  8378  oaass  8491  brinxper  8668  iiner  8731  xpdom2  9005  ssenen  9084  pssnn  9098  hartogs  9454  card2on  9464  ackbij1  10154  cfub  10166  fin23lem27  10245  fin1a2lem11  10327  fin1a2lem13  10329  hsmexlem2  10344  zorn2lem4  10416  ondomon  10480  gchina  10617  intgru  10732  ingru  10733  addclprlem2  10935  psslinpr  10949  ltexprlem3  10956  ltexprlem4  10957  reclem2pr  10966  suplem1pr  10970  sup2  12107  nnind  12187  nnunb  12428  uzind  12616  xmullem2  13212  xrsupsslem  13254  xrinfmsslem  13255  seqof  14016  hashfacen  14411  sswrd  14479  wrdind  14679  wrd2ind  14680  pfxccatin12lem2  14688  cau3lem  15312  caubnd  15316  sumodd  16352  vdwnnlem2  16962  ramub2  16980  fthres2  17896  oduprs  18261  odupos  18287  chnrss  18576  chndss  18577  cycsubm  19172  lsmdisj2  19652  gsumxp2  19950  pgpfac1lem3  20049  nrhmzr  20509  subrgdvds  20558  lspdisj  21119  lspprat  21147  lbsextlem2  21153  ocv2ss  21667  ocvin  21668  coe1fzgsumd  22283  evl1gsumd  22336  tgcl  22948  epttop  22988  cmpsub  23379  tgcmp  23380  hauscmplem  23385  dfconn2  23398  llyss  23458  nllyss  23459  locfincmp  23505  txcnpi  23587  txcnp  23599  snfil  23843  fgcl  23857  filconn  23862  filuni  23864  cfinfil  23872  csdfil  23873  supfil  23874  ufildom1  23905  fin1aufil  23911  fmfnfmlem3  23935  ptcmplem2  24032  cldsubg  24090  iscau3  25259  iscau4  25260  caussi  25278  volfiniun  25528  plycj  26256  plycjOLD  26258  abelth  26423  wilthlem2  27050  lgsdir2lem4  27309  gausslemma2dlem0i  27345  gausslemma2dlem1a  27346  pntleml  27592  ltsres  27644  nosupno  27685  noinfno  27700  noseqinds  28303  uhgr0vsize0  29326  cusgrfilem2  29544  uhgrvd00  29622  clwwisshclwws  30104  frcond3  30358  frgrncvvdeqlem2  30389  lpni  30570  ubthlem1  30960  chintcli  31421  h1de2i  31643  spansnm0i  31740  strlem1  32340  mdslmd1i  32419  reuxfrdf  32579  n0nsnel  32604  disjss1f  32661  disjpreima  32673  ssrelf  32707  suppss3  32815  nnindf  32912  wrdt2ind  33032  crefss  34013  esumpcvgval  34242  cbvex1v  35236  r1filim  35267  onvf1odlem4  35308  subgrtrl  35335  subgrpth  35336  subgrcycl  35337  derangenlem  35373  connpconn  35437  cvmsss2  35476  pocnv  35965  wzel  36024  in-ax8  36426  naim1  36591  naim2  36592  waj-ax  36616  lukshef-ax2  36617  ttctr  36695  dfttc2g  36708  bj-exim  36924  bj-sbievw1  37172  wl-dfcleq  37848  poimirlem26  37985  poimirlem30  37989  poimirlem32  37991  itg2addnclem  38010  ismtybndlem  38145  ablo4pnp  38219  isdrngo3  38298  keridl  38371  ispridl2  38377  ispridlc  38409  trcoss  38911  funALTVss  39123  disjss  39170  eldisjss  39177  prter1  39343  lshpdisj  39451  snatpsubN  40214  pmapglb2N  40235  pmapglb2xN  40236  elpaddn0  40264  sn-sup2  42954  nna4b4nsq  43111  mzpindd  43196  pellexlem3  43281  pellexlem5  43283  pellex  43285  2nn0ind  43395  lnr2i  43566  ofoaid1  43808  ofoaid2  43809  intabssd  43968  iunrelexpuztr  44168  hess  44229  frege52aid  44307  frege52b  44338  neik0pk1imk0  44496  relpmin  45401  rankrelp  45409  n0nsn2el  47489  imasetpreimafvbijlemfv1  47879  isubgredg  48358  stgrusgra  48451  isubgr3stgrlem6  48463  iinfsubc  49549  elsetrecslem  50190