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	syl5bi 241	. 2 ⊢ (𝜑 → (𝜃 → 𝜒))
4		3imtr4g.3	. 2 ⊢ (𝜏 ↔ 𝜒)
5	3, 4	syl6ibr 251	1 ⊢ (𝜑 → (𝜃 → 𝜏))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  3anim123d  1442  3orim123d  1443  sbi1  2075  moim  2545  mo3  2565  2euswapv  2633  2euswap  2648  exists2  2664  nelcon3d  3062  ral2imi  3083  ralimdv2  3108  reximdv2  3200  reximd2a  3246  moeq3  3648  rmoim  3676  2reuswap  3682  2reuswap2  3683  2rmoswap  3697  ssel  3915  sselOLD  3916  sstr2  3929  ssrexf  3986  ssrmof  3987  ss2abdvALT  3999  sscon  4074  ssdif  4075  unss1  4114  ssrin  4168  difin0ss  4303  r19.2z  4426  sspw  4547  uniss  4848  ssuni  4867  intssuni  4902  iinssiun  4938  iunss1  4939  iinss1  4940  ss2iun  4943  iunxdif3  5025  disjss2  5043  disjss1  5046  disjss3  5074  ssbrd  5118  poss  5506  pofun  5522  soss  5524  frss  5557  sess1  5558  sess2  5559  wess  5577  relss  5693  ssrel2  5697  ssrelrel  5708  relop  5762  dmss  5814  dmcosseq  5885  funss  6460  fss  6626  fun  6645  brprcneu  6773  brprcneuALT  6774  f1eqcocnv  7182  f1eqcocnvOLD  7183  isores3  7215  isomin  7217  isopolem  7225  isosolem  7227  isowe2  7230  ovmpos  7430  dfwe2  7633  epweon  7634  onint  7649  orduniorsuc  7686  trom  7730  finds  7754  finds2  7756  f1oweALT  7824  tposfn2  8073  tposfo2  8074  tposf1o2  8077  fprlem2  8126  smores  8192  tz7.48lem  8281  tz7.48-3  8284  oaass  8401  iiner  8587  xpdom2  8863  ssenen  8947  pssnn  8960  pssnnOLD  9049  hartogs  9312  card2on  9322  ackbij1  10003  cfub  10014  fin23lem27  10093  fin1a2lem11  10175  fin1a2lem13  10177  hsmexlem2  10192  zorn2lem4  10264  ondomon  10328  gchina  10464  intgru  10579  ingru  10580  addclprlem2  10782  psslinpr  10796  ltexprlem3  10803  ltexprlem4  10804  reclem2pr  10813  suplem1pr  10817  sup2  11940  nnind  12000  nnunb  12238  uzind  12421  xmullem2  13008  xrsupsslem  13050  xrinfmsslem  13051  seqof  13789  hashfacen  14175  hashfacenOLD  14176  sswrd  14234  wrdind  14444  wrd2ind  14445  pfxccatin12lem2  14453  cau3lem  15075  caubnd  15079  sumodd  16106  vdwnnlem2  16706  ramub2  16724  fthres2  17657  odupos  18055  cycsubm  18830  lsmdisj2  19297  gsumxp2  19590  pgpfac1lem3  19689  subrgdvds  20047  lspdisj  20396  lspprat  20424  lbsextlem2  20430  ocv2ss  20887  ocvin  20888  coe1fzgsumd  21482  evl1gsumd  21532  tgcl  22128  epttop  22168  cmpsub  22560  tgcmp  22561  hauscmplem  22566  dfconn2  22579  llyss  22639  nllyss  22640  locfincmp  22686  txcnpi  22768  txcnp  22780  snfil  23024  fgcl  23038  filconn  23043  filuni  23045  cfinfil  23053  csdfil  23054  supfil  23055  ufildom1  23086  fin1aufil  23092  fmfnfmlem3  23116  ptcmplem2  23213  cldsubg  23271  iscau3  24451  iscau4  24452  caussi  24470  volfiniun  24720  plycj  25447  abelth  25609  wilthlem2  26227  lgsdir2lem4  26485  gausslemma2dlem0i  26521  gausslemma2dlem1a  26522  pntleml  26768  uhgr0vsize0  27615  cusgrfilem2  27832  uhgrvd00  27910  clwwisshclwws  28388  frcond3  28642  frgrncvvdeqlem2  28673  lpni  28851  ubthlem1  29241  chintcli  29702  h1de2i  29924  spansnm0i  30021  strlem1  30621  mdslmd1i  30700  reuxfrdf  30848  rabss3d  30870  disjss1f  30920  disjpreima  30932  ssrelf  30964  suppss3  31068  nnindf  31142  wrdt2ind  31234  oduprs  31251  crefss  31808  esumpcvgval  32055  subgrtrl  33104  subgrpth  33105  subgrcycl  33106  derangenlem  33142  connpconn  33206  cvmsss2  33245  pocnv  33739  wzel  33827  sltres  33874  nosupno  33915  noinfno  33930  nocvxmin  33982  naim1  34587  naim2  34588  waj-ax  34612  lukshef-ax2  34613  bj-eximALT  34831  bj-sbievw1  35038  poimirlem26  35812  poimirlem30  35816  poimirlem32  35818  itg2addnclem  35837  ismtybndlem  35973  ablo4pnp  36047  isdrngo3  36126  keridl  36199  ispridl2  36205  ispridlc  36237  trcoss  36607  funALTVss  36817  disjss  36849  eldisjss  36856  prter1  36900  lshpdisj  37008  snatpsubN  37771  pmapglb2N  37792  pmapglb2xN  37793  elpaddn0  37821  sn-sup2  40446  nna4b4nsq  40504  mzpindd  40575  pellexlem3  40660  pellexlem5  40662  pellex  40664  2nn0ind  40774  lnr2i  40948  intabssd  41133  iunrelexpuztr  41334  hess  41395  frege52aid  41473  frege52b  41504  neik0pk1imk0  41664  imasetpreimafvbijlemfv1  44866  nrhmzr  45442  elsetrecslem  46415