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  2544  mo3  2564  2euswapv  2630  2euswap  2645  exists2  2662  nelcon3d  3040  ral2imi  3076  ralimdv2  3146  reximdv2  3147  reximd2a  3247  moeq3  3658  rmoim  3686  2reuswap  3692  2reuswap2  3693  2rmoswap  3707  ssel  3915  sstr2OLD  3929  ssrexf  3988  ssrmof  3989  ssralv  3990  ssrexv  3991  ss2abim  4000  ss2abdv  4005  rabss3d  4021  sscon  4083  ssdif  4084  unss1  4125  ssrin  4182  difin0ss  4313  r19.2z  4439  sspw  4552  uniss  4858  ssuni  4875  intssuni  4912  iinssiun  4947  iunss1  4948  iinss1  4949  ss2iun  4952  iunxdif3  5037  disjss2  5055  disjss1  5058  disjss3  5084  ssbrd  5128  poss  5541  pofun  5557  soss  5559  frss  5595  sess1  5596  sess2  5597  wess  5617  relss  5738  ssrel2  5741  ssrelrel  5752  relop  5805  dmss  5857  dmcosseq  5933  dmcosseqOLD  5934  dmcosseqOLDOLD  5935  funss  6517  f1imadifssran  6584  fss  6684  fun  6702  brprcneu  6830  brprcneuALT  6831  f1eqcocnv  7256  isores3  7290  isomin  7292  isopolem  7300  isosolem  7302  isowe2  7305  ovmpos  7515  dfwe2  7728  epweon  7729  onint  7744  orduniorsuc  7781  trom  7826  finds  7847  finds2  7849  f1oweALT  7925  tposfn2  8198  tposfo2  8199  tposf1o2  8202  fprlem2  8251  smores  8292  tz7.48lem  8380  tz7.48-3  8383  oaass  8496  brinxper  8673  iiner  8736  xpdom2  9010  ssenen  9089  pssnn  9103  hartogs  9459  card2on  9469  ackbij1  10159  cfub  10171  fin23lem27  10250  fin1a2lem11  10332  fin1a2lem13  10334  hsmexlem2  10349  zorn2lem4  10421  ondomon  10485  gchina  10622  intgru  10737  ingru  10738  addclprlem2  10940  psslinpr  10954  ltexprlem3  10961  ltexprlem4  10962  reclem2pr  10971  suplem1pr  10975  sup2  12112  nnind  12192  nnunb  12433  uzind  12621  xmullem2  13217  xrsupsslem  13259  xrinfmsslem  13260  seqof  14021  hashfacen  14416  sswrd  14484  wrdind  14684  wrd2ind  14685  pfxccatin12lem2  14693  cau3lem  15317  caubnd  15321  sumodd  16357  vdwnnlem2  16967  ramub2  16985  fthres2  17901  oduprs  18266  odupos  18292  chnrss  18581  chndss  18582  cycsubm  19177  lsmdisj2  19657  gsumxp2  19955  pgpfac1lem3  20054  nrhmzr  20514  subrgdvds  20563  lspdisj  21123  lspprat  21151  lbsextlem2  21157  ocv2ss  21653  ocvin  21654  coe1fzgsumd  22269  evl1gsumd  22322  tgcl  22934  epttop  22974  cmpsub  23365  tgcmp  23366  hauscmplem  23371  dfconn2  23384  llyss  23444  nllyss  23445  locfincmp  23491  txcnpi  23573  txcnp  23585  snfil  23829  fgcl  23843  filconn  23848  filuni  23850  cfinfil  23858  csdfil  23859  supfil  23860  ufildom1  23891  fin1aufil  23897  fmfnfmlem3  23921  ptcmplem2  24018  cldsubg  24076  iscau3  25245  iscau4  25246  caussi  25264  volfiniun  25514  plycj  26242  plycjOLD  26244  abelth  26406  wilthlem2  27032  lgsdir2lem4  27291  gausslemma2dlem0i  27327  gausslemma2dlem1a  27328  pntleml  27574  ltsres  27626  nosupno  27667  noinfno  27682  noseqinds  28285  uhgr0vsize0  29308  cusgrfilem2  29525  uhgrvd00  29603  clwwisshclwws  30085  frcond3  30339  frgrncvvdeqlem2  30370  lpni  30551  ubthlem1  30941  chintcli  31402  h1de2i  31624  spansnm0i  31721  strlem1  32321  mdslmd1i  32400  reuxfrdf  32560  n0nsnel  32585  disjss1f  32642  disjpreima  32654  ssrelf  32688  suppss3  32796  nnindf  32893  wrdt2ind  33013  crefss  33993  esumpcvgval  34222  cbvex1v  35216  r1filim  35247  onvf1odlem4  35288  subgrtrl  35315  subgrpth  35316  subgrcycl  35317  derangenlem  35353  connpconn  35417  cvmsss2  35456  pocnv  35945  wzel  36004  in-ax8  36406  naim1  36571  naim2  36572  waj-ax  36596  lukshef-ax2  36597  ttctr  36675  dfttc2g  36688  bj-exim  36904  bj-sbievw1  37152  wl-dfcleq  37830  poimirlem26  37967  poimirlem30  37971  poimirlem32  37973  itg2addnclem  37992  ismtybndlem  38127  ablo4pnp  38201  isdrngo3  38280  keridl  38353  ispridl2  38359  ispridlc  38391  trcoss  38893  funALTVss  39105  disjss  39152  eldisjss  39159  prter1  39325  lshpdisj  39433  snatpsubN  40196  pmapglb2N  40217  pmapglb2xN  40218  elpaddn0  40246  sn-sup2  42936  nna4b4nsq  43093  mzpindd  43178  pellexlem3  43259  pellexlem5  43261  pellex  43263  2nn0ind  43373  lnr2i  43544  ofoaid1  43786  ofoaid2  43787  intabssd  43946  iunrelexpuztr  44146  hess  44207  frege52aid  44285  frege52b  44316  neik0pk1imk0  44474  relpmin  45379  rankrelp  45387  n0nsn2el  47473  imasetpreimafvbijlemfv1  47863  isubgredg  48342  stgrusgra  48435  isubgr3stgrlem6  48447  iinfsubc  49533  elsetrecslem  50174