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  4701  unielrel  6276  predtrss  6324  fvrnressn  7162  fconst5  7209  soisores  7330  caofrss  7719  caoftrn  7721  f1o2ndf1  8130  oaord  8568  omord2  8588  omcan  8590  oeord  8609  oecan  8610  nnaord  8640  nnmord  8653  omsmo  8679  pmss12g  8892  cantnf  9716  pm54.43  10024  ttukeylem2  10533  axlttrn  11316  axltadd  11317  axmulgt0  11318  axsup  11319  ltadd2  11348  ltord1  11772  recex  11878  ltmul1  12100  lt2msq  12136  nnge1  12277  zltp1le  12651  uzss  12884  eluzp1m1  12887  prodge0rd  13125  ixxssixx  13384  zesq  14248  pfxccatin12lem3  14753  swrdccat3blem  14760  relexpsucnnr  15047  climrlim2  15566  rlimres  15577  climshftlem  15593  lo1add  15646  lo1mul  15647  rlimsqzlem  15668  lo1le  15671  isercolllem2  15685  isercoll  15687  climsup  15689  cvgcmp  15835  climcndslem1  15868  dvds1lem  16288  sumodd  16408  rprpwr  16579  algcvg  16596  eucalgcvga  16606  rpexp12i  16744  crth  16798  pc2dvds  16900  pcmpt  16913  prmpwdvds  16925  1arith  16948  vdwlem2  17003  vdwlem6  17007  vdwlem8  17009  ercpbl  17570  initoid  18022  termoid  18023  ipopos  18555  insubm  18805  subginv  19125  symggrp  19391  f1otrspeq  19438  lsmless1x  19635  lsmless2x  19636  dprdss  20022  rngpropd  20144  dvdsunit  20352  irredrmul  20400  isdrngd  20738  isdrngdOLD  20740  lspextmo  21028  rngqiprngimf1lem  21271  domnchr  21514  zntoslem  21542  evlseu  22074  mat2pmatf1  22702  tgss  22941  neips  23086  opnnei  23093  lpss3  23117  ssrest  23149  t1t0  23321  kgen2ss  23528  isfild  23831  fgss  23846  fgss2  23847  cnpflf2  23973  fclsss1  23995  fclsss2  23996  tgpt0  24092  tsmsxp  24128  prdsxmslem2  24505  ngptgp  24612  nghmcn  24721  qdensere  24745  evth  24946  nmhmcn  25108  tcphcph  25226  caussi  25286  equivcfil  25288  rrxmvallem  25393  ivthlem2  25442  ovollb2lem  25478  ovolunlem1  25487  volun  25535  ioombl1lem4  25551  volsup2  25595  volcn  25596  ismbf3d  25644  itg2mulclem  25736  cpnord  25926  lhop1  26008  aaliou3lem2  26340  ulmclm  26385  ulmss  26395  abelth  26440  cosord  26528  efif1olem4  26542  argimgt0  26609  logdivlt  26618  cxploglim  26976  dvdssqf  27136  mumullem1  27177  mumullem2  27178  bposlem6  27288  lgsdchr  27354  gausslemma2dlem1a  27364  m1lgs  27387  chtppilim  27474  sletr  27758  sletric  27764  madebdayim  27881  madebdaylemold  27891  sltlpss  27900  om2noseqf1o  28262  ax5seg  28902  axpasch  28905  axlowdimlem16  28921  axeuclid  28927  axcontlem4  28931  usgr1v0e  29290  nb3gr2nb  29348  cplgr1v  29394  finsumvtxdg2size  29515  usgr2pthlem  29730  clwwlknwwlksn  30004  erclwwlknsym  30036  erclwwlkntr  30037  frgr3vlem1  30239  3vfriswmgrlem  30243  numclwwlk5  30354  minvecolem5  30847  ocsh  31249  shless  31325  leopadd  32098  leopmuli  32099  leopmul2i  32101  leoptr  32103  spansncv2  32259  mdsl0  32276  ssdmd1  32279  cvdmd  32303  cdj3i  32407  uzssico  32733  expgt0b  32765  eqgvscpbl  33319  qusvscpbl  33320  cmpcref  33790  acycgrsubgr  35104  cvmliftmolem1  35227  satffunlem2lem2  35352  mrsubff1  35460  msubff1  35502  lediv2aALT  35623  cgr3tr4  35994  colinearxfr  36017  lineext  36018  brsegle  36050  seglecgr12im  36052  segletr  36056  colinbtwnle  36060  outsideoftr  36071  lineelsb2  36090  ivthALT  36277  tailfb  36319  poimirlem29  37597  itg2addnclem  37619  itg2addnclem3  37621  itg2addnc  37622  incsequz  37696  mettrifi  37705  ismtycnv  37750  bfplem1  37770  ghomco  37839  rngoisocnv  37929  keridl  37980  dmncan1  38024  ax12indalem  38887  ax12inda2ALT  38888  omllaw4  39188  cmtcomlemN  39190  cvlexch2  39271  cvlatexch2  39279  cvrexch  39363  atexchltN  39384  3atlem5  39430  lplnribN  39494  linepsubN  39695  paddss1  39760  paddss2  39761  pmapjoin  39795  pmapjat1  39796  cdleme36a  40403  dib2dim  41186  dih2dimbALTN  41188  djhcvat42  41358  dihjatcclem4  41364  dihjat1lem  41371  lcfrlem6  41490  hlhillcs  41905  oexpreposd  42302  mulgt0b2d  42435  pell1234qrmulcl  42811  pell14qrss1234  42812  pell14qrmulcl  42819  pell14qrreccl  42820  pell1qrss14  42824  monotoddzzfi  42899  oddcomabszz  42901  omabs2  43290  omcl3g  43292  tfsconcat0b  43304  naddwordnexlem4  43359  climinf  45566  2ffzoeq  47285  iccpartgt  47360  upwlkwlk  48001  uspgrsprf1  48009  rrx2xpref1o  48585  itschlc0yqe  48627  resipos  48820