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 ⊢ (𝜑 → (𝜃 → 𝜏))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  3anim123d  1471  3orim123d  1472  sbi1  2105  moim  2572  mo3  2592  2euswapv  2658  2euswap  2673  exists2  2689  nelcon3d  3068  ral2imi  3104  ralimdv2  3174  reximdv2  3175  reximd2a  3275  moeq3  3675  rmoim  3703  2reuswap  3709  2reuswap2  3710  2rmoswap  3724  ssel  3931  ssrexf  4004  ssrmof  4005  ssralv  4006  ssrexv  4007  ss2abim  4014  ss2abdv  4019  rabss3d  4035  sscon  4097  ssdif  4098  unss1  4138  ssrin  4194  difin0ss  4328  r19.2z  4460  sspw  4573  uniss  4880  ssuni  4898  intssuni  4935  iinssiun  4970  iunss1  4971  iinss1  4972  ss2iun  4975  iunxdif3  5061  disjss2  5079  disjss1  5082  disjss3  5108  ssbrd  5154  poss  5571  pofun  5587  soss  5589  frss  5625  sess1  5626  sess2  5627  wess  5647  relss  5768  ssrel2  5771  ssrelrel  5782  relop  5836  dmss  5892  dmcosseq  5968  dmcosseqOLD  5969  funss  6555  fss  6722  fun  6740  brprcneu  6871  brprcneuALT  6872  f1eqcocnv  7299  isores3  7333  isomin  7335  isopolem  7343  isosolem  7345  isowe2  7348  ovmpos  7558  dfwe2  7769  epweon  7770  onint  7785  orduniorsuc  7822  trom  7867  finds  7889  finds2  7891  f1oweALT  7965  tposfn2  8240  tposfo2  8241  tposf1o2  8244  fprlem2  8294  smores  8335  tz7.48lem  8424  tz7.48-3  8427  oaass  8542  brinxper  8720  iiner  8783  xpdom2  9056  ssenen  9135  pssnn  9149  hartogs  9502  card2on  9512  ackbij1  10225  cfub  10236  fin23lem27  10316  fin1a2lem11  10398  fin1a2lem13  10400  hsmexlem2  10415  zorn2lem4  10487  ondomon  10551  gchina  10688  intgru  10803  ingru  10804  addclprlem2  11006  psslinpr  11020  ltexprlem3  11027  ltexprlem4  11028  reclem2pr  11037  suplem1pr  11041  sup2  12175  nnind  12255  nnunb  12504  uzind  12692  xmullem2  13295  xrsupsslem  13337  xrinfmsslem  13338  seqof  14100  hashfacen  14496  sswrd  14564  wrdind  14764  wrd2ind  14765  pfxccatin12lem2  14773  cau3lem  15411  caubnd  15415  sumodd  16450  vdwnnlem2  17060  ramub2  17078  fthres2  17995  oduprs  18360  odupos  18386  chnrss  18675  chndss  18676  cycsubm  19277  lsmdisj2  19756  gsumxp2  20054  pgpfac1lem3  20153  nrhmzr  20645  subrgdvds  20694  isdrng5  20863  lspdisj  21258  lspprat  21286  lbsextlem2  21292  ocv2ss  21832  ocvin  21833  coe1fzgsumd  22473  evl1gsumd  22526  tgcl  23135  epttop  23175  cmpsub  23566  tgcmp  23567  hauscmplem  23572  dfconn2  23585  llyss  23645  nllyss  23646  locfincmp  23692  txcnpi  23774  txcnp  23786  snfil  24030  fgcl  24044  filconn  24049  filuni  24051  cfinfil  24059  csdfil  24060  supfil  24061  ufildom1  24092  fin1aufil  24098  fmfnfmlem3  24122  ptcmplem2  24219  cldsubg  24277  iscau3  25446  iscau4  25447  caussi  25465  volfiniun  25715  plycj  26443  plycjOLD  26445  abelth  26613  wilthlem2  27242  lgsdir2lem4  27501  gausslemma2dlem0i  27537  gausslemma2dlem1a  27538  pntleml  27784  ltsres  27835  nosupno  27876  noinfno  27891  noseqinds  28495  plngrotlem2  29079  uhgr0vsize0  29598  cusgrfilem2  29815  uhgrvd00  29893  clwwisshclwws  30375  frcond3  30629  frgrncvvdeqlem2  30660  lpni  30841  ubthlem1  31231  chintcli  31692  h1de2i  31914  spansnm0i  32011  strlem1  32611  mdslmd1i  32690  reuxfrdf  32846  n0nsnel  32870  disjss1f  32926  disjpreima  32938  ssrelf  32969  suppss3  33077  nnindf  33173  wrdt2ind  33282  crefss  34248  esumpcvgval  34477  cbvex1v  35471  r1filim  35507  onvf1odlem4  35598  subgrtrl  35633  subgrpth  35634  subgrcycl  35635  derangenlem  35671  connpconn  35735  cvmsss2  35774  pocnv  36263  wzel  36322  in-ax8  36764  naim1  36928  naim2  36929  waj-ax  36953  lukshef-ax2  36954  ttctr  37032  dfttc2g  37045  bj-exim  37260  bj-sbievw1  37508  wl-dfcleq  38188  poimirlem26  38325  poimirlem30  38329  poimirlem32  38331  itg2addnclem  38350  ismtybndlem  38485  ablo4pnp  38559  isdrngo3  38638  keridl  38711  ispridl2  38717  ispridlc  38749  trcoss  39249  funALTVss  39461  disjss  39508  eldisjss  39515  prter1  39681  lshpdisj  39789  snatpsubN  40552  pmapglb2N  40573  pmapglb2xN  40574  elpaddn0  40602  sn-sup2  43293  nna4b4nsq  43420  mzpindd  43505  pellexlem3  43586  pellexlem5  43588  pellex  43590  2nn0ind  43700  lnr2i  43871  ofoaid1  44113  ofoaid2  44114  intabssd  44273  iunrelexpuztr  44473  hess  44534  frege52aid  44612  frege52b  44643  neik0pk1imk0  44801  relpmin  45689  rankrelp  45697  n0nsn2el  47790  imasetpreimafvbijlemfv1  48180  isubgredg  48659  stgrusgra  48752  isubgr3stgrlem6  48764  iinfsubc  49864  elsetrecslem  50505