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  2569  mo3  2589  2euswapv  2655  2euswap  2670  exists2  2686  nelcon3d  3065  ral2imi  3101  ralimdv2  3171  reximdv2  3172  reximd2a  3272  moeq3  3670  rmoim  3698  2reuswap  3704  2reuswap2  3705  2rmoswap  3719  ssel  3925  ssrexf  3998  ssrmof  3999  ssralv  4000  ssrexv  4001  ss2abim  4008  ss2abdv  4013  rabss3d  4029  sscon  4090  ssdif  4091  unss1  4131  ssrin  4187  difin0ss  4321  r19.2z  4455  sspw  4568  uniss  4875  ssuni  4893  intssuni  4930  iinssiun  4965  iunss1  4966  iinss1  4967  ss2iun  4970  iunxdif3  5055  disjss2  5073  disjss1  5076  disjss3  5102  ssbrd  5148  poss  5565  pofun  5581  soss  5583  frss  5619  sess1  5620  sess2  5621  wess  5641  relss  5762  ssrel2  5765  ssrelrel  5776  relop  5832  dmss  5888  dmcosseq  5964  dmcosseqOLD  5965  funss  6554  fss  6722  fun  6740  brprcneu  6871  brprcneuALT  6872  f1eqcocnv  7305  isores3  7339  isomin  7341  isopolem  7349  isosolem  7351  isowe2  7354  ovmpos  7564  dfwe2  7779  epweon  7780  onint  7795  orduniorsuc  7832  trom  7877  finds  7899  finds2  7901  f1oweALT  7975  tposfn2  8251  tposfo2  8252  tposf1o2  8255  fprlem2  8305  smores  8346  tz7.48lemOLD  8437  tz7.48-3  8440  oaass  8555  brinxper  8733  iiner  8796  xpdom2  9077  ssenen  9156  pssnn  9170  hartogs  9523  card2on  9533  ackbij1  10264  cfub  10275  fin23lem27  10355  fin1a2lem11  10437  fin1a2lem13  10439  hsmexlem2  10454  zorn2lem4  10526  ondomon  10596  gchina  10733  intgru  10848  ingru  10849  addclprlem2  11051  psslinpr  11065  ltexprlem3  11072  ltexprlem4  11073  reclem2pr  11082  suplem1pr  11086  sup2  12220  nnind  12300  nnunb  12549  uzind  12738  xmullem2  13342  xrsupsslem  13384  xrinfmsslem  13385  seqof  14148  hashfacen  14544  sswrd  14612  wrdind  14816  wrd2ind  14817  pfxccatin12lem2  14825  cau3lem  15467  caubnd  15471  sumodd  16503  vdwnnlem2  17113  ramub2  17131  fthres2  18048  oduprs  18413  odupos  18439  chnrss  18728  chndss  18729  cycsubm  19356  lsmdisj2  19835  gsumxp2  20133  pgpfac1lem3  20232  nrhmzr  20728  subrgdvds  20777  isdrng5  20947  lspdisj  21342  lspprat  21370  lbsextlem2  21376  ocv2ss  21918  ocvin  21919  coe1fzgsumd  22561  evl1gsumd  22614  tgcl  23226  epttop  23266  cmpsub  23657  tgcmp  23658  hauscmplem  23663  dfconn2  23676  llyss  23737  nllyss  23738  locfincmp  23784  txcnpi  23866  txcnp  23878  snfil  24122  fgcl  24136  filconn  24141  filuni  24143  cfinfil  24151  csdfil  24152  supfil  24153  ufildom1  24184  fin1aufil  24190  fmfnfmlem3  24214  ptcmplem2  24311  cldsubg  24369  iscau3  25538  iscau4  25539  caussi  25557  volfiniun  25807  plycj  26535  plycjOLD  26537  abelth  26709  wilthlem2  27337  lgsdir2lem4  27596  gausslemma2dlem0i  27632  gausslemma2dlem1a  27633  pntleml  27879  ltsres  27930  nosupno  27971  noinfno  27986  noseqinds  28590  plngrotlem2  29177  uhgr0vsize0  29731  cusgrfilem2  29948  uhgrvd00  30026  subgrtrl  30205  subgrpth  30267  subgrcycl  30296  clwwisshclwws  30517  frcond3  30781  frgrncvvdeqlem2  30812  lpni  30993  ubthlem1  31383  chintcli  31844  h1de2i  32066  spansnm0i  32163  strlem1  32763  mdslmd1i  32842  reuxfrdf  32998  n0nsnel  33022  disjss1f  33077  disjpreima  33089  ssrelf  33120  suppss3  33226  nnindf  33322  wrdt2ind  33427  crefss  34392  esumpcvgval  34621  cbvex1v  35616  r1filim  35645  onvf1odlem4  35786  derangenlem  35833  connpconn  35897  cvmsss2  35936  pocnv  36425  wzel  36484  in-ax8  36911  naim1  37075  naim2  37076  waj-ax  37100  lukshef-ax2  37101  ttctr  37179  dfttc2g  37192  bj-exim  37407  bj-sbievw1  37655  wl-dfcleq  38333  poimirlem26  38460  poimirlem30  38464  poimirlem32  38466  itg2addnclem  38485  ismtybndlem  38621  ablo4pnp  38695  isdrngo3  38774  keridl  38847  ispridl2  38853  ispridlc  38885  trcoss  39385  funALTVss  39597  disjss  39644  eldisjss  39651  prter1  39817  lshpdisj  39925  snatpsubN  40688  pmapglb2N  40709  pmapglb2xN  40710  elpaddn0  40738  sn-sup2  43444  nna4b4nsq  43571  mzpindd  43656  pellexlem3  43737  pellexlem5  43739  pellex  43741  2nn0ind  43851  lnr2i  44022  ofoaid1  44264  ofoaid2  44265  intabssd  44424  iunrelexpuztr  44624  hess  44685  frege52aid  44763  frege52b  44794  neik0pk1imk0  44952  relpmin  45840  rankrelp  45848  n0nsn2el  47978  imasetpreimafvbijlemfv1  48368  isubgredg  48847  stgrusgra  48940  isubgr3stgrlem6  48952  iinfsubc  50049  elsetrecslem  50690