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  1442  3orim123d  1443  sbi1  2069  moim  2542  mo3  2562  2euswapv  2628  2euswap  2643  exists2  2660  nelcon3d  3048  ral2imi  3083  ralimdv2  3161  reximdv2  3162  reximd2a  3267  moeq3  3721  rmoim  3749  2reuswap  3755  2reuswap2  3756  2rmoswap  3770  ssel  3989  sstr2OLD  4003  ssrexf  4062  ssrmof  4063  ssralv  4064  ssrexv  4065  ss2abdv  4076  rabss3d  4091  sscon  4153  ssdif  4154  unss1  4195  ssrin  4250  difin0ss  4379  r19.2z  4501  sspw  4616  uniss  4920  ssuni  4937  intssuni  4975  iinssiun  5010  iunss1  5011  iinss1  5012  ss2iun  5015  iunxdif3  5100  disjss2  5118  disjss1  5121  disjss3  5147  ssbrd  5191  poss  5599  pofun  5615  soss  5617  frss  5653  sess1  5654  sess2  5655  wess  5675  relss  5794  ssrel2  5798  ssrelrel  5809  relop  5864  dmss  5916  dmcosseq  5990  dmcosseqOLD  5991  funss  6587  fss  6753  fun  6771  brprcneu  6897  brprcneuALT  6898  f1eqcocnv  7321  isores3  7355  isomin  7357  isopolem  7365  isosolem  7367  isowe2  7370  ovmpos  7581  dfwe2  7793  epweon  7794  onint  7810  orduniorsuc  7850  trom  7896  finds  7919  finds2  7921  f1oweALT  7996  tposfn2  8272  tposfo2  8273  tposf1o2  8276  fprlem2  8325  smores  8391  tz7.48lem  8480  tz7.48-3  8483  oaass  8598  brinxper  8773  iiner  8828  xpdom2  9106  ssenen  9190  pssnn  9207  hartogs  9582  card2on  9592  ackbij1  10275  cfub  10287  fin23lem27  10366  fin1a2lem11  10448  fin1a2lem13  10450  hsmexlem2  10465  zorn2lem4  10537  ondomon  10601  gchina  10737  intgru  10852  ingru  10853  addclprlem2  11055  psslinpr  11069  ltexprlem3  11076  ltexprlem4  11077  reclem2pr  11086  suplem1pr  11090  sup2  12222  nnind  12282  nnunb  12520  uzind  12708  xmullem2  13304  xrsupsslem  13346  xrinfmsslem  13347  seqof  14097  hashfacen  14490  sswrd  14557  wrdind  14757  wrd2ind  14758  pfxccatin12lem2  14766  cau3lem  15390  caubnd  15394  sumodd  16422  vdwnnlem2  17030  ramub2  17048  fthres2  17986  oduprs  18358  odupos  18386  cycsubm  19233  lsmdisj2  19715  gsumxp2  20013  pgpfac1lem3  20112  nrhmzr  20554  subrgdvds  20603  lspdisj  21145  lspprat  21173  lbsextlem2  21179  ocv2ss  21709  ocvin  21710  coe1fzgsumd  22324  evl1gsumd  22377  tgcl  22992  epttop  23032  cmpsub  23424  tgcmp  23425  hauscmplem  23430  dfconn2  23443  llyss  23503  nllyss  23504  locfincmp  23550  txcnpi  23632  txcnp  23644  snfil  23888  fgcl  23902  filconn  23907  filuni  23909  cfinfil  23917  csdfil  23918  supfil  23919  ufildom1  23950  fin1aufil  23956  fmfnfmlem3  23980  ptcmplem2  24077  cldsubg  24135  iscau3  25326  iscau4  25327  caussi  25345  volfiniun  25596  plycj  26332  plycjOLD  26334  abelth  26500  wilthlem2  27127  lgsdir2lem4  27387  gausslemma2dlem0i  27423  gausslemma2dlem1a  27424  pntleml  27670  sltres  27722  nosupno  27763  noinfno  27778  nocvxmin  27838  noseqinds  28314  uhgr0vsize0  29271  cusgrfilem2  29489  uhgrvd00  29567  clwwisshclwws  30044  frcond3  30298  frgrncvvdeqlem2  30329  lpni  30509  ubthlem1  30899  chintcli  31360  h1de2i  31582  spansnm0i  31679  strlem1  32279  mdslmd1i  32358  reuxfrdf  32519  n0nsnel  32543  disjss1f  32592  disjpreima  32604  ssrelf  32635  suppss3  32742  nnindf  32826  wrdt2ind  32923  crefss  33810  esumpcvgval  34059  cbvex1v  35067  subgrtrl  35118  subgrpth  35119  subgrcycl  35120  derangenlem  35156  connpconn  35220  cvmsss2  35259  pocnv  35743  wzel  35806  in-ax8  36207  naim1  36372  naim2  36373  waj-ax  36397  lukshef-ax2  36398  bj-eximALT  36624  bj-sbievw1  36828  poimirlem26  37633  poimirlem30  37637  poimirlem32  37639  itg2addnclem  37658  ismtybndlem  37793  ablo4pnp  37867  isdrngo3  37946  keridl  38019  ispridl2  38025  ispridlc  38057  trcoss  38464  funALTVss  38681  disjss  38713  eldisjss  38720  prter1  38861  lshpdisj  38969  snatpsubN  39733  pmapglb2N  39754  pmapglb2xN  39755  elpaddn0  39783  ss2ab1  42237  sn-sup2  42478  nna4b4nsq  42647  mzpindd  42734  pellexlem3  42819  pellexlem5  42821  pellex  42823  2nn0ind  42934  lnr2i  43105  ofoaid1  43348  ofoaid2  43349  intabssd  43509  iunrelexpuztr  43709  hess  43770  frege52aid  43848  frege52b  43879  neik0pk1imk0  44037  n0nsn2el  46975  imasetpreimafvbijlemfv1  47328  isubgredg  47790  stgrusgra  47862  isubgr3stgrlem6  47874  elsetrecslem  48930