Theorem 3imtr4d 293

Description: More general version of 3imtr4i 291. Useful for converting conditional definitions in a formula. (Contributed by NM, 26-Oct-1995.)

Hypotheses

Ref	Expression
3imtr4d.1	⊢ (𝜑 → (𝜓 → 𝜒))
3imtr4d.2	⊢ (𝜑 → (𝜃 ↔ 𝜓))
3imtr4d.3	⊢ (𝜑 → (𝜏 ↔ 𝜒))

Assertion

Ref	Expression
3imtr4d	⊢ (𝜑 → (𝜃 → 𝜏))

Proof of Theorem 3imtr4d

Step	Hyp	Ref	Expression
1		3imtr4d.2	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜓))
2		3imtr4d.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3		3imtr4d.3	. . 3 ⊢ (𝜑 → (𝜏 ↔ 𝜒))
4	2, 3	sylibrd 258	. 2 ⊢ (𝜑 → (𝜓 → 𝜏))
5	1, 4	sylbid 239	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:  rmosn  4722  unielrel  6272  predtrss  6322  fvrnressn  7160  fconst5  7208  soisores  7326  caofrss  7708  caoftrn  7710  f1o2ndf1  8110  oaord  8549  omord2  8569  omcan  8571  oeord  8590  oecan  8591  nnaord  8621  nnmord  8634  omsmo  8659  pmss12g  8865  cantnf  9690  pm54.43  9998  ttukeylem2  10507  axlttrn  11290  axltadd  11291  axmulgt0  11292  axsup  11293  ltadd2  11322  ltord1  11744  recex  11850  ltmul1  12068  lt2msq  12103  nnge1  12244  zltp1le  12616  uzss  12849  eluzp1m1  12852  prodge0rd  13085  ixxssixx  13342  zesq  14193  pfxccatin12lem3  14686  swrdccat3blem  14693  relexpsucnnr  14976  climrlim2  15495  rlimres  15506  climshftlem  15522  lo1add  15575  lo1mul  15576  rlimsqzlem  15599  lo1le  15602  isercolllem2  15616  isercoll  15618  climsup  15620  cvgcmp  15766  climcndslem1  15799  dvds1lem  16215  sumodd  16335  rprpwr  16504  algcvg  16517  eucalgcvga  16527  rpexp12i  16665  crth  16715  pc2dvds  16816  pcmpt  16829  prmpwdvds  16841  1arith  16864  vdwlem2  16919  vdwlem6  16923  vdwlem8  16925  ercpbl  17499  initoid  17955  termoid  17956  ipopos  18493  insubm  18735  subginv  19049  symggrp  19309  f1otrspeq  19356  lsmless1x  19553  lsmless2x  19554  dprdss  19940  rngpropd  20068  dvdsunit  20270  irredrmul  20318  isdrngd  20533  isdrngdOLD  20535  lspextmo  20811  rngqiprngimf1lem  21053  domnchr  21303  zntoslem  21331  evlseu  21865  mat2pmatf1  22451  tgss  22691  neips  22837  opnnei  22844  lpss3  22868  ssrest  22900  t1t0  23072  kgen2ss  23279  isfild  23582  fgss  23597  fgss2  23598  cnpflf2  23724  fclsss1  23746  fclsss2  23747  tgpt0  23843  tsmsxp  23879  prdsxmslem2  24258  ngptgp  24365  nghmcn  24482  qdensere  24506  evth  24705  nmhmcn  24867  tcphcph  24985  caussi  25045  equivcfil  25047  rrxmvallem  25152  ivthlem2  25201  ovollb2lem  25237  ovolunlem1  25246  volun  25294  ioombl1lem4  25310  volsup2  25354  volcn  25355  ismbf3d  25403  itg2mulclem  25496  cpnord  25685  lhop1  25766  aaliou3lem2  26092  ulmclm  26135  ulmss  26145  abelth  26189  cosord  26276  efif1olem4  26290  argimgt0  26356  logdivlt  26365  cxploglim  26718  dvdssqf  26878  mumullem1  26919  mumullem2  26920  bposlem6  27028  lgsdchr  27094  gausslemma2dlem1a  27104  m1lgs  27127  chtppilim  27214  sletr  27497  sletric  27503  madebdayim  27619  madebdaylemold  27629  sltlpss  27638  ax5seg  28463  axpasch  28466  axlowdimlem16  28482  axeuclid  28488  axcontlem4  28492  usgr1v0e  28850  nb3gr2nb  28908  cplgr1v  28954  finsumvtxdg2size  29074  usgr2pthlem  29287  clwwlknwwlksn  29558  erclwwlknsym  29590  erclwwlkntr  29591  frgr3vlem1  29793  3vfriswmgrlem  29797  numclwwlk5  29908  minvecolem5  30401  ocsh  30803  shless  30879  leopadd  31652  leopmuli  31653  leopmul2i  31655  leoptr  31657  spansncv2  31813  mdsl0  31830  ssdmd1  31833  cvdmd  31857  cdj3i  31961  uzssico  32262  eqgvscpbl  32735  qusvscpbl  32736  cmpcref  33128  acycgrsubgr  34447  cvmliftmolem1  34570  satffunlem2lem2  34695  mrsubff1  34803  msubff1  34845  lediv2aALT  34960  cgr3tr4  35328  colinearxfr  35351  lineext  35352  brsegle  35384  seglecgr12im  35386  segletr  35390  colinbtwnle  35394  outsideoftr  35405  lineelsb2  35424  ivthALT  35523  tailfb  35565  poimirlem29  36820  itg2addnclem  36842  itg2addnclem3  36844  itg2addnc  36845  incsequz  36919  mettrifi  36928  ismtycnv  36973  bfplem1  36993  ghomco  37062  rngoisocnv  37152  keridl  37203  dmncan1  37247  ax12indalem  38118  ax12inda2ALT  38119  omllaw4  38419  cmtcomlemN  38421  cvlexch2  38502  cvlatexch2  38510  cvrexch  38594  atexchltN  38615  3atlem5  38661  lplnribN  38725  linepsubN  38926  paddss1  38991  paddss2  38992  pmapjoin  39026  pmapjat1  39027  cdleme36a  39634  dib2dim  40417  dih2dimbALTN  40419  djhcvat42  40589  dihjatcclem4  40595  dihjat1lem  40602  lcfrlem6  40721  hlhillcs  41136  oexpreposd  41514  mulgt0b2d  41635  pell1234qrmulcl  41895  pell14qrss1234  41896  pell14qrmulcl  41903  pell14qrreccl  41904  pell1qrss14  41908  monotoddzzfi  41983  oddcomabszz  41985  omabs2  42384  omcl3g  42386  tfsconcat0b  42398  naddwordnexlem4  42454  climinf  44620  2ffzoeq  46334  iccpartgt  46393  upwlkwlk  46815  uspgrsprf1  46823  rrx2xpref1o  47491  itschlc0yqe  47533