Theorem 3imtr4d 297

Description: More general version of 3imtr4i 295. 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 262	. 2 ⊢ (𝜑 → (𝜓 → 𝜏))
5	1, 4	sylbid 243	1 ⊢ (𝜑 → (𝜃 → 𝜏))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  rmosn  4687  unielrel  6273  predtrss  6321  fvrnressn  7156  fconst5  7202  soisores  7323  caofrss  7711  caoftrn  7713  f1o2ndf1  8113  oaord  8528  omord2  8548  omcan  8550  oeord  8570  oecan  8571  nnaord  8601  nnmord  8614  omsmo  8640  pmss12g  8863  cantnf  9658  pm54.43  9983  ttukeylem2  10490  axlttrn  11278  axltadd  11279  axmulgt0  11280  axsup  11281  ltadd2  11310  ltord1  11736  recex  11842  ltmul1  12061  lt2msq  12096  nnge1  12260  zltp1le  12640  uzss  12881  eluzp1m1  12884  prodge0rd  13121  ixxssixx  13382  zesq  14258  pfxccatin12lem3  14765  swrdccat3blem  14772  relexpsucnnr  15058  climrlim2  15594  rlimres  15605  climshftlem  15621  lo1add  15674  lo1mul  15675  rlimsqzlem  15696  lo1le  15699  isercolllem2  15713  isercoll  15715  climsup  15717  cvgcmp  15864  climcndslem1  15899  dvds1lem  16321  sumodd  16442  rprpwr  16613  algcvg  16630  eucalgcvga  16640  rpexp12i  16779  crth  16833  pc2dvds  16935  pcmpt  16948  prmpwdvds  16960  1arith  16983  vdwlem2  17038  vdwlem6  17042  vdwlem8  17044  ercpbl  17599  initoid  18054  termoid  18055  ipopos  18588  insubm  18873  subginv  19195  symggrp  19466  f1otrspeq  19513  lsmless1x  19710  lsmless2x  19711  dprdss  20097  rngpropd  20248  dvdsunit  20457  irredrmul  20505  isdrngd  20843  isdrngdOLD  20845  lspextmo  21151  rngqiprngimf1lem  21401  domnchr  21647  zntoslem  21671  evlseu  22199  mat2pmatf1  22851  tgss  23090  neips  23235  opnnei  23242  lpss3  23266  ssrest  23298  t1t0  23470  kgen2ss  23677  isfild  23980  fgss  23995  fgss2  23996  cnpflf2  24122  fclsss1  24144  fclsss2  24145  tgpt0  24241  tsmsxp  24277  prdsxmslem2  24651  ngptgp  24758  nghmcn  24867  qdensere  24891  evth  25083  nmhmcn  25244  tcphcph  25361  caussi  25421  equivcfil  25423  rrxmvallem  25528  ivthlem2  25576  ovollb2lem  25612  ovolunlem1  25621  volun  25669  ioombl1lem4  25685  volsup2  25729  volcn  25730  ismbf3d  25778  itg2mulclem  25870  cpnord  26059  lhop1  26138  aaliou3lem2  26469  ulmclm  26512  ulmss  26522  abelth  26566  cosord  26658  efif1olem4  26672  argimgt0  26739  logdivlt  26748  cxploglim  27104  dvdssqf  27264  mumullem1  27305  mumullem2  27306  bposlem6  27415  lgsdchr  27481  gausslemma2dlem1a  27491  m1lgs  27514  chtppilim  27601  lestr  27888  lestric  27894  madebdayim  28043  madebdaylemold  28053  ltslpss  28063  om2noseqf1o  28456  zsoring  28564  bdaypw2n0bndlem  28618  bdayfin  28642  ax5seg  29225  axpasch  29228  axlowdimlem16  29244  axeuclid  29250  axcontlem4  29254  usgr1v0e  29613  nb3gr2nb  29671  cplgr1v  29717  finsumvtxdg2size  29837  usgr2pthlem  30049  clwwlknwwlksn  30326  erclwwlknsym  30358  erclwwlkntr  30359  frgr3vlem1  30561  3vfriswmgrlem  30565  numclwwlk5  30676  minvecolem5  31170  ocsh  31572  shless  31648  leopadd  32421  leopmuli  32422  leopmul2i  32424  leoptr  32426  spansncv2  32582  mdsl0  32599  ssdmd1  32602  cvdmd  32626  cdj3i  32730  uzssico  33066  expgt0b  33098  eqgvscpbl  33609  qusvscpbl  33610  cmpcref  34181  acycgrsubgr  35545  cvmliftmolem1  35668  satffunlem2lem2  35793  mrsubff1  35901  msubff1  35943  lediv2aALT  36064  cgr3tr4  36439  colinearxfr  36462  lineext  36463  brsegle  36495  seglecgr12im  36497  segletr  36501  colinbtwnle  36505  outsideoftr  36516  lineelsb2  36535  ivthALT  36731  tailfb  36773  poimirlem29  38183  itg2addnclem  38205  itg2addnclem3  38207  itg2addnc  38208  incsequz  38282  mettrifi  38291  ismtycnv  38336  bfplem1  38356  ghomco  38425  rngoisocnv  38515  keridl  38566  dmncan1  38610  ax12indalem  39604  ax12inda2ALT  39605  omllaw4  39905  cmtcomlemN  39907  cvlexch2  39988  cvlatexch2  39996  cvrexch  40079  atexchltN  40100  3atlem5  40146  lplnribN  40210  linepsubN  40411  paddss1  40476  paddss2  40477  pmapjoin  40511  pmapjat1  40512  cdleme36a  41119  dib2dim  41902  dih2dimbALTN  41904  djhcvat42  42074  dihjatcclem4  42080  dihjat1lem  42087  lcfrlem6  42206  hlhillcs  42617  oexpreposd  42968  mulgt0b1d  43131  mullt0b1d  43142  pell1234qrmulcl  43469  pell14qrss1234  43470  pell14qrmulcl  43477  pell14qrreccl  43478  pell1qrss14  43482  monotoddzzfi  43556  oddcomabszz  43558  omabs2  43946  omcl3g  43948  tfsconcat0b  43960  naddwordnexlem4  44015  climinf  46209  2ffzoeq  47949  iccpartgt  48060  pgnbgreunbgrlem1  48762  pgnbgreunbgrlem4  48768  upwlkwlk  48788  uspgrsprf1  48796  rrx2xpref1o  49378  itschlc0yqe  49420  resipos  49633