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  2108  moim  2574  mo3  2594  2euswapv  2660  2euswap  2675  exists2  2691  nelcon3d  3070  ral2imi  3106  ralimdv2  3176  reximdv2  3177  reximd2a  3277  moeq3  3677  rmoim  3705  2reuswap  3711  2reuswap2  3712  2rmoswap  3726  ssel  3932  ssrexf  4005  ssrmof  4006  ssralv  4007  ssrexv  4008  ss2abim  4015  ss2abdv  4020  rabss3d  4036  sscon  4097  ssdif  4098  unss1  4138  ssrin  4194  difin0ss  4328  r19.2z  4462  sspw  4575  uniss  4882  ssuni  4900  intssuni  4937  iinssiun  4972  iunss1  4973  iinss1  4974  ss2iun  4977  iunxdif3  5063  disjss2  5081  disjss1  5084  disjss3  5110  ssbrd  5156  poss  5573  pofun  5589  soss  5591  frss  5627  sess1  5628  sess2  5629  wess  5649  relss  5770  ssrel2  5773  ssrelrel  5784  relop  5838  dmss  5894  dmcosseq  5970  dmcosseqOLD  5971  funss  6560  fss  6727  fun  6745  brprcneu  6876  brprcneuALT  6877  f1eqcocnv  7309  isores3  7343  isomin  7345  isopolem  7353  isosolem  7355  isowe2  7358  ovmpos  7568  dfwe2  7780  epweon  7781  onint  7796  orduniorsuc  7833  trom  7878  finds  7900  finds2  7902  f1oweALT  7976  tposfn2  8251  tposfo2  8252  tposf1o2  8255  fprlem2  8305  smores  8346  tz7.48lem  8435  tz7.48-3  8438  oaass  8553  brinxper  8731  iiner  8794  xpdom2  9068  ssenen  9147  pssnn  9161  hartogs  9514  card2on  9524  ackbij1  10237  cfub  10248  fin23lem27  10328  fin1a2lem11  10410  fin1a2lem13  10412  hsmexlem2  10427  zorn2lem4  10499  ondomon  10567  gchina  10704  intgru  10819  ingru  10820  addclprlem2  11022  psslinpr  11036  ltexprlem3  11043  ltexprlem4  11044  reclem2pr  11053  suplem1pr  11057  sup2  12191  nnind  12271  nnunb  12520  uzind  12709  xmullem2  13312  xrsupsslem  13354  xrinfmsslem  13355  seqof  14118  hashfacen  14514  sswrd  14582  wrdind  14786  wrd2ind  14787  pfxccatin12lem2  14795  cau3lem  15435  caubnd  15439  sumodd  16473  vdwnnlem2  17083  ramub2  17101  fthres2  18018  oduprs  18383  odupos  18409  chnrss  18698  chndss  18699  cycsubm  19322  lsmdisj2  19801  gsumxp2  20099  pgpfac1lem3  20198  nrhmzr  20691  subrgdvds  20740  isdrng5  20909  lspdisj  21304  lspprat  21332  lbsextlem2  21338  ocv2ss  21878  ocvin  21879  coe1fzgsumd  22519  evl1gsumd  22572  tgcl  23181  epttop  23221  cmpsub  23612  tgcmp  23613  hauscmplem  23618  dfconn2  23631  llyss  23692  nllyss  23693  locfincmp  23739  txcnpi  23821  txcnp  23833  snfil  24077  fgcl  24091  filconn  24096  filuni  24098  cfinfil  24106  csdfil  24107  supfil  24108  ufildom1  24139  fin1aufil  24145  fmfnfmlem3  24169  ptcmplem2  24266  cldsubg  24324  iscau3  25493  iscau4  25494  caussi  25512  volfiniun  25762  plycj  26490  plycjOLD  26492  abelth  26660  wilthlem2  27289  lgsdir2lem4  27548  gausslemma2dlem0i  27584  gausslemma2dlem1a  27585  pntleml  27831  ltsres  27882  nosupno  27923  noinfno  27938  noseqinds  28542  plngrotlem2  29126  uhgr0vsize0  29652  cusgrfilem2  29869  uhgrvd00  29947  subgrtrl  30126  subgrpth  30188  subgrcycl  30217  clwwisshclwws  30438  frcond3  30696  frgrncvvdeqlem2  30727  lpni  30908  ubthlem1  31298  chintcli  31759  h1de2i  31981  spansnm0i  32078  strlem1  32678  mdslmd1i  32757  reuxfrdf  32913  n0nsnel  32937  disjss1f  32993  disjpreima  33005  ssrelf  33036  suppss3  33143  nnindf  33239  wrdt2ind  33344  crefss  34308  esumpcvgval  34537  cbvex1v  35532  r1filim  35561  onvf1odlem4  35652  derangenlem  35705  connpconn  35769  cvmsss2  35808  pocnv  36297  wzel  36356  in-ax8  36798  naim1  36962  naim2  36963  waj-ax  36987  lukshef-ax2  36988  ttctr  37066  dfttc2g  37079  bj-exim  37294  bj-sbievw1  37542  wl-dfcleq  38222  poimirlem26  38359  poimirlem30  38363  poimirlem32  38365  itg2addnclem  38384  ismtybndlem  38520  ablo4pnp  38594  isdrngo3  38673  keridl  38746  ispridl2  38752  ispridlc  38784  trcoss  39284  funALTVss  39496  disjss  39543  eldisjss  39550  prter1  39716  lshpdisj  39824  snatpsubN  40587  pmapglb2N  40608  pmapglb2xN  40609  elpaddn0  40637  sn-sup2  43343  nna4b4nsq  43470  mzpindd  43555  pellexlem3  43636  pellexlem5  43638  pellex  43640  2nn0ind  43750  lnr2i  43921  ofoaid1  44163  ofoaid2  44164  intabssd  44323  iunrelexpuztr  44523  hess  44584  frege52aid  44662  frege52b  44693  neik0pk1imk0  44851  relpmin  45739  rankrelp  45747  n0nsn2el  47840  imasetpreimafvbijlemfv1  48230  isubgredg  48709  stgrusgra  48802  isubgr3stgrlem6  48814  iinfsubc  49913  elsetrecslem  50554