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  4716  unielrel  6262  predtrss  6312  fvrnressn  7143  fconst5  7191  soisores  7308  caofrss  7689  caoftrn  7691  f1o2ndf1  8090  oaord  8530  omord2  8550  omcan  8552  oeord  8571  oecan  8572  nnaord  8602  nnmord  8615  omsmo  8640  pmss12g  8846  cantnf  9670  pm54.43  9978  ttukeylem2  10487  axlttrn  11268  axltadd  11269  axmulgt0  11270  axsup  11271  ltadd2  11300  ltord1  11722  recex  11828  ltmul1  12046  lt2msq  12081  nnge1  12222  zltp1le  12594  uzss  12827  eluzp1m1  12830  prodge0rd  13063  ixxssixx  13320  zesq  14171  pfxccatin12lem3  14664  swrdccat3blem  14671  relexpsucnnr  14954  climrlim2  15473  rlimres  15484  climshftlem  15500  lo1add  15553  lo1mul  15554  rlimsqzlem  15577  lo1le  15580  isercolllem2  15594  isercoll  15596  climsup  15598  cvgcmp  15744  climcndslem1  15777  dvds1lem  16193  sumodd  16313  rprpwr  16482  algcvg  16495  eucalgcvga  16505  rpexp12i  16643  crth  16693  pc2dvds  16794  pcmpt  16807  prmpwdvds  16819  1arith  16842  vdwlem2  16897  vdwlem6  16901  vdwlem8  16903  ercpbl  17477  initoid  17933  termoid  17934  ipopos  18471  insubm  18675  subginv  18985  symggrp  19232  f1otrspeq  19279  lsmless1x  19476  lsmless2x  19477  dprdss  19858  dvdsunit  20145  irredrmul  20191  isdrngd  20297  isdrngdOLD  20299  lspextmo  20616  domnchr  21017  zntoslem  21045  evlseu  21575  mat2pmatf1  22160  tgss  22400  neips  22546  opnnei  22553  lpss3  22577  ssrest  22609  t1t0  22781  kgen2ss  22988  isfild  23291  fgss  23306  fgss2  23307  cnpflf2  23433  fclsss1  23455  fclsss2  23456  tgpt0  23552  tsmsxp  23588  prdsxmslem2  23967  ngptgp  24074  nghmcn  24191  qdensere  24215  evth  24404  nmhmcn  24565  tcphcph  24683  caussi  24743  equivcfil  24745  rrxmvallem  24850  ivthlem2  24898  ovollb2lem  24934  ovolunlem1  24943  volun  24991  ioombl1lem4  25007  volsup2  25051  volcn  25052  ismbf3d  25100  itg2mulclem  25193  cpnord  25381  lhop1  25460  aaliou3lem2  25785  ulmclm  25828  ulmss  25838  abelth  25882  cosord  25969  efif1olem4  25983  argimgt0  26049  logdivlt  26058  cxploglim  26409  dvdssqf  26569  mumullem1  26610  mumullem2  26611  bposlem6  26719  lgsdchr  26785  gausslemma2dlem1a  26795  m1lgs  26818  chtppilim  26905  sletr  27188  sletric  27194  madebdayim  27305  madebdaylemold  27315  sltlpss  27324  ax5seg  28061  axpasch  28064  axlowdimlem16  28080  axeuclid  28086  axcontlem4  28090  usgr1v0e  28448  nb3gr2nb  28506  cplgr1v  28552  finsumvtxdg2size  28672  usgr2pthlem  28885  clwwlknwwlksn  29156  erclwwlknsym  29188  erclwwlkntr  29189  frgr3vlem1  29391  3vfriswmgrlem  29395  numclwwlk5  29506  minvecolem5  29997  ocsh  30399  shless  30475  leopadd  31248  leopmuli  31249  leopmul2i  31251  leoptr  31253  spansncv2  31409  mdsl0  31426  ssdmd1  31429  cvdmd  31453  cdj3i  31557  uzssico  31866  eqgvscpbl  32327  qusvscpbl  32328  cmpcref  32661  acycgrsubgr  33980  cvmliftmolem1  34103  satffunlem2lem2  34228  mrsubff1  34336  msubff1  34378  lediv2aALT  34493  cgr3tr4  34854  colinearxfr  34877  lineext  34878  brsegle  34910  seglecgr12im  34912  segletr  34916  colinbtwnle  34920  outsideoftr  34931  lineelsb2  34950  ivthALT  35024  tailfb  35066  poimirlem29  36321  itg2addnclem  36343  itg2addnclem3  36345  itg2addnc  36346  incsequz  36421  mettrifi  36430  ismtycnv  36475  bfplem1  36495  ghomco  36564  rngoisocnv  36654  keridl  36705  dmncan1  36749  ax12indalem  37620  ax12inda2ALT  37621  omllaw4  37921  cmtcomlemN  37923  cvlexch2  38004  cvlatexch2  38012  cvrexch  38096  atexchltN  38117  3atlem5  38163  lplnribN  38227  linepsubN  38428  paddss1  38493  paddss2  38494  pmapjoin  38528  pmapjat1  38529  cdleme36a  39136  dib2dim  39919  dih2dimbALTN  39921  djhcvat42  40091  dihjatcclem4  40097  dihjat1lem  40104  lcfrlem6  40223  hlhillcs  40638  oexpreposd  40993  mulgt0b2d  41115  pell1234qrmulcl  41364  pell14qrss1234  41365  pell14qrmulcl  41372  pell14qrreccl  41373  pell1qrss14  41377  monotoddzzfi  41452  oddcomabszz  41454  omabs2  41853  omcl3g  41855  tfsconcat0b  41867  naddwordnexlem4  41923  climinf  44095  2ffzoeq  45808  iccpartgt  45867  upwlkwlk  46289  uspgrsprf1  46297  rrx2xpref1o  47052  itschlc0yqe  47094