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  2072  moim  2537  mo3  2557  2euswapv  2623  2euswap  2638  exists2  2655  nelcon3d  3033  ral2imi  3068  ralimdv2  3142  reximdv2  3143  reximd2a  3247  moeq3  3683  rmoim  3711  2reuswap  3717  2reuswap2  3718  2rmoswap  3732  ssel  3940  sstr2OLD  3954  ssrexf  4013  ssrmof  4014  ssralv  4015  ssrexv  4016  ss2abdv  4029  rabss3d  4044  sscon  4106  ssdif  4107  unss1  4148  ssrin  4205  difin0ss  4336  r19.2z  4458  sspw  4574  uniss  4879  ssuni  4896  intssuni  4934  iinssiun  4969  iunss1  4970  iinss1  4971  ss2iun  4974  iunxdif3  5059  disjss2  5077  disjss1  5080  disjss3  5106  ssbrd  5150  poss  5548  pofun  5564  soss  5566  frss  5602  sess1  5603  sess2  5604  wess  5624  relss  5744  ssrel2  5748  ssrelrel  5759  relop  5814  dmss  5866  dmcosseq  5940  dmcosseqOLD  5941  funss  6535  f1imadifssran  6602  fss  6704  fun  6722  brprcneu  6848  brprcneuALT  6849  f1eqcocnv  7276  isores3  7310  isomin  7312  isopolem  7320  isosolem  7322  isowe2  7325  ovmpos  7537  dfwe2  7750  epweon  7751  onint  7766  orduniorsuc  7805  trom  7851  finds  7872  finds2  7874  f1oweALT  7951  tposfn2  8227  tposfo2  8228  tposf1o2  8231  fprlem2  8280  smores  8321  tz7.48lem  8409  tz7.48-3  8412  oaass  8525  brinxper  8700  iiner  8762  xpdom2  9036  ssenen  9115  pssnn  9132  hartogs  9497  card2on  9507  ackbij1  10190  cfub  10202  fin23lem27  10281  fin1a2lem11  10363  fin1a2lem13  10365  hsmexlem2  10380  zorn2lem4  10452  ondomon  10516  gchina  10652  intgru  10767  ingru  10768  addclprlem2  10970  psslinpr  10984  ltexprlem3  10991  ltexprlem4  10992  reclem2pr  11001  suplem1pr  11005  sup2  12139  nnind  12204  nnunb  12438  uzind  12626  xmullem2  13225  xrsupsslem  13267  xrinfmsslem  13268  seqof  14024  hashfacen  14419  sswrd  14487  wrdind  14687  wrd2ind  14688  pfxccatin12lem2  14696  cau3lem  15321  caubnd  15325  sumodd  16358  vdwnnlem2  16967  ramub2  16985  fthres2  17896  oduprs  18261  odupos  18287  cycsubm  19134  lsmdisj2  19612  gsumxp2  19910  pgpfac1lem3  20009  nrhmzr  20446  subrgdvds  20495  lspdisj  21035  lspprat  21063  lbsextlem2  21069  ocv2ss  21582  ocvin  21583  coe1fzgsumd  22191  evl1gsumd  22244  tgcl  22856  epttop  22896  cmpsub  23287  tgcmp  23288  hauscmplem  23293  dfconn2  23306  llyss  23366  nllyss  23367  locfincmp  23413  txcnpi  23495  txcnp  23507  snfil  23751  fgcl  23765  filconn  23770  filuni  23772  cfinfil  23780  csdfil  23781  supfil  23782  ufildom1  23813  fin1aufil  23819  fmfnfmlem3  23843  ptcmplem2  23940  cldsubg  23998  iscau3  25178  iscau4  25179  caussi  25197  volfiniun  25448  plycj  26183  plycjOLD  26185  abelth  26351  wilthlem2  26979  lgsdir2lem4  27239  gausslemma2dlem0i  27275  gausslemma2dlem1a  27276  pntleml  27522  sltres  27574  nosupno  27615  noinfno  27630  nocvxmin  27690  noseqinds  28187  uhgr0vsize0  29166  cusgrfilem2  29384  uhgrvd00  29462  clwwisshclwws  29944  frcond3  30198  frgrncvvdeqlem2  30229  lpni  30409  ubthlem1  30799  chintcli  31260  h1de2i  31482  spansnm0i  31579  strlem1  32179  mdslmd1i  32258  reuxfrdf  32420  n0nsnel  32444  disjss1f  32501  disjpreima  32513  ssrelf  32543  suppss3  32647  nnindf  32744  wrdt2ind  32875  crefss  33839  esumpcvgval  34068  cbvex1v  35064  onvf1odlem4  35093  subgrtrl  35120  subgrpth  35121  subgrcycl  35122  derangenlem  35158  connpconn  35222  cvmsss2  35261  pocnv  35750  wzel  35812  in-ax8  36212  naim1  36377  naim2  36378  waj-ax  36402  lukshef-ax2  36403  bj-eximALT  36629  bj-sbievw1  36833  poimirlem26  37640  poimirlem30  37644  poimirlem32  37646  itg2addnclem  37665  ismtybndlem  37800  ablo4pnp  37874  isdrngo3  37953  keridl  38026  ispridl2  38032  ispridlc  38064  trcoss  38473  funALTVss  38691  disjss  38723  eldisjss  38730  prter1  38872  lshpdisj  38980  snatpsubN  39744  pmapglb2N  39765  pmapglb2xN  39766  elpaddn0  39794  ss2ab1  42207  sn-sup2  42479  nna4b4nsq  42648  mzpindd  42734  pellexlem3  42819  pellexlem5  42821  pellex  42823  2nn0ind  42934  lnr2i  43105  ofoaid1  43347  ofoaid2  43348  intabssd  43508  iunrelexpuztr  43708  hess  43769  frege52aid  43847  frege52b  43878  neik0pk1imk0  44036  relpmin  44942  rankrelp  44950  n0nsn2el  47026  imasetpreimafvbijlemfv1  47404  isubgredg  47866  stgrusgra  47958  isubgr3stgrlem6  47970  iinfsubc  49047  elsetrecslem  49688