Theorem 3imtr4d 294

Description: More general version of 3imtr4i 292. 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 259	. 2 ⊢ (𝜑 → (𝜓 → 𝜏))
5	1, 4	sylbid 240	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:  rmosn  4667  unielrel  6216  predtrss  6264  fvrnressn  7089  fconst5  7135  soisores  7256  caofrss  7644  caoftrn  7646  f1o2ndf1  8047  oaord  8457  omord2  8477  omcan  8479  oeord  8498  oecan  8499  nnaord  8529  nnmord  8542  omsmo  8568  pmss12g  8788  cantnf  9578  pm54.43  9889  ttukeylem2  10396  axlttrn  11180  axltadd  11181  axmulgt0  11182  axsup  11183  ltadd2  11212  ltord1  11638  recex  11744  ltmul1  11966  lt2msq  12002  nnge1  12148  zltp1le  12517  uzss  12750  eluzp1m1  12753  prodge0rd  12994  ixxssixx  13254  zesq  14128  pfxccatin12lem3  14634  swrdccat3blem  14641  relexpsucnnr  14927  climrlim2  15449  rlimres  15460  climshftlem  15476  lo1add  15529  lo1mul  15530  rlimsqzlem  15551  lo1le  15554  isercolllem2  15568  isercoll  15570  climsup  15572  cvgcmp  15718  climcndslem1  15751  dvds1lem  16173  sumodd  16294  rprpwr  16465  algcvg  16482  eucalgcvga  16492  rpexp12i  16630  crth  16684  pc2dvds  16786  pcmpt  16799  prmpwdvds  16811  1arith  16834  vdwlem2  16889  vdwlem6  16893  vdwlem8  16895  ercpbl  17448  initoid  17903  termoid  17904  ipopos  18437  insubm  18721  subginv  19041  symggrp  19307  f1otrspeq  19354  lsmless1x  19551  lsmless2x  19552  dprdss  19938  rngpropd  20087  dvdsunit  20292  irredrmul  20340  isdrngd  20675  isdrngdOLD  20677  lspextmo  20985  rngqiprngimf1lem  21226  domnchr  21464  zntoslem  21488  evlseu  22013  mat2pmatf1  22639  tgss  22878  neips  23023  opnnei  23030  lpss3  23054  ssrest  23086  t1t0  23258  kgen2ss  23465  isfild  23768  fgss  23783  fgss2  23784  cnpflf2  23910  fclsss1  23932  fclsss2  23933  tgpt0  24029  tsmsxp  24065  prdsxmslem2  24439  ngptgp  24546  nghmcn  24655  qdensere  24679  evth  24880  nmhmcn  25042  tcphcph  25159  caussi  25219  equivcfil  25221  rrxmvallem  25326  ivthlem2  25375  ovollb2lem  25411  ovolunlem1  25420  volun  25468  ioombl1lem4  25484  volsup2  25528  volcn  25529  ismbf3d  25577  itg2mulclem  25669  cpnord  25859  lhop1  25941  aaliou3lem2  26273  ulmclm  26318  ulmss  26328  abelth  26373  cosord  26462  efif1olem4  26476  argimgt0  26543  logdivlt  26552  cxploglim  26910  dvdssqf  27070  mumullem1  27111  mumullem2  27112  bposlem6  27222  lgsdchr  27288  gausslemma2dlem1a  27298  m1lgs  27321  chtppilim  27408  sletr  27692  sletric  27698  madebdayim  27828  madebdaylemold  27838  sltlpss  27848  om2noseqf1o  28226  zsoring  28327  ax5seg  28911  axpasch  28914  axlowdimlem16  28930  axeuclid  28936  axcontlem4  28940  usgr1v0e  29299  nb3gr2nb  29357  cplgr1v  29403  finsumvtxdg2size  29524  usgr2pthlem  29736  clwwlknwwlksn  30010  erclwwlknsym  30042  erclwwlkntr  30043  frgr3vlem1  30245  3vfriswmgrlem  30249  numclwwlk5  30360  minvecolem5  30853  ocsh  31255  shless  31331  leopadd  32104  leopmuli  32105  leopmul2i  32107  leoptr  32109  spansncv2  32265  mdsl0  32282  ssdmd1  32285  cvdmd  32309  cdj3i  32413  uzssico  32759  expgt0b  32791  eqgvscpbl  33307  qusvscpbl  33308  cmpcref  33855  acycgrsubgr  35194  cvmliftmolem1  35317  satffunlem2lem2  35442  mrsubff1  35550  msubff1  35592  lediv2aALT  35713  cgr3tr4  36086  colinearxfr  36109  lineext  36110  brsegle  36142  seglecgr12im  36144  segletr  36148  colinbtwnle  36152  outsideoftr  36163  lineelsb2  36182  ivthALT  36369  tailfb  36411  poimirlem29  37689  itg2addnclem  37711  itg2addnclem3  37713  itg2addnc  37714  incsequz  37788  mettrifi  37797  ismtycnv  37842  bfplem1  37862  ghomco  37931  rngoisocnv  38021  keridl  38072  dmncan1  38116  ax12indalem  38984  ax12inda2ALT  38985  omllaw4  39285  cmtcomlemN  39287  cvlexch2  39368  cvlatexch2  39376  cvrexch  39459  atexchltN  39480  3atlem5  39526  lplnribN  39590  linepsubN  39791  paddss1  39856  paddss2  39857  pmapjoin  39891  pmapjat1  39892  cdleme36a  40499  dib2dim  41282  dih2dimbALTN  41284  djhcvat42  41454  dihjatcclem4  41460  dihjat1lem  41467  lcfrlem6  41586  hlhillcs  41997  oexpreposd  42355  mulgt0b1d  42505  mullt0b1d  42516  pell1234qrmulcl  42888  pell14qrss1234  42889  pell14qrmulcl  42896  pell14qrreccl  42897  pell1qrss14  42901  monotoddzzfi  42975  oddcomabszz  42977  omabs2  43365  omcl3g  43367  tfsconcat0b  43379  naddwordnexlem4  43434  climinf  45646  2ffzoeq  47358  iccpartgt  47458  pgnbgreunbgrlem1  48144  pgnbgreunbgrlem4  48150  upwlkwlk  48170  uspgrsprf1  48178  rrx2xpref1o  48750  itschlc0yqe  48792  resipos  49006